To address a most important point, as suggested by Andrej Bauer, Lean's intended model is one where types are sets. Mario Carneiro showed in his master's thesis that Lean has such a set-theoretic model (specifically using ZFC plus infinitely many large cardinals). So that means Lean is consistent (assuming no bugs in its implementation), and a theorem in Lean means what a classical mathematician would think it means (once they interpret types as sets and understand universes).
The failure of normalization however means that one can't give a more computational model of Lean, which isn't a large deal since Lean is mostly used as a classical mathematics proof assistant. Also, it should be pointed out that Lean's reduction (in Lean 3 at least) is painfully slow anyway. It can barely add numbers with #reduce, so non-termination and slow termination are basically the same in the eyes of the user. This is discussed in this Zulip thread.
A related issue which you also address, comes down to elimination outside of Lean's Prop. Unlike your expectation, Lean does have a limited form of large elimination called (syntactic) subsingleton elimination.
As a quick aside, my understanding is that there are two interpretations of definitional equality in Lean. One is what is actually implemented in Lean. Mario's thesis has an approximation of that which is decidable, but it breaks transitivity. Broken defeq transitivity implies broken subject reduction. The other definitional equality which appears in Mario's thesis is a more ideal one. It satisfies transitivity and subject reduction, but it is undecidable.
The reason for this failure of subject reduction in Lean's implemented type theory, to my understanding, is that Lean has proof irrelevance (similar to Coq's SProp) and a syntactic form of subsingleton elimination as described in this document. In particular, the latter lets you eliminate "syntactic subsingletons" such as true, false, and, =, and acc (which is related to well-founded) to types in Type. These are called "syntactic subsingletons" since they have at most one type constructor. As Pierre-Marie Pédrot pointed out, this leads to the issues with definitional equality that I mention above. On Zulip, Mario gave a MWE of how to use proof irrelevance of Prop and the syntactic subsingleton elimination of acc to explicitly break transitivity of defeq, break subject reduction, and fool Lean tactics into producing false terms (but which the kernel still correctly rejects).
These issues are relatively small for Lean users. Again, they don't break consistency or change the set-theoretic model, just make some things more annoying for users. Lean users rarely notice these issues are there (and likely couldn't point to them at all), but they do occasionally come up as discussed here. Mario, however likes to point out that it is possible to run into the same issues even in a system without explicitly broken definitional equality. In particular, it is easy to construct examples where a = b and b = c are fast to compute definitionally, but a definitional proof of a = c is quite slow and will time out. While not technically a failure of definitional equality, it is the same sort of issue in practice. One must resort to an alternate proof of a = c in some cases.
(Also, it should be pointed out that even Coq has some issues with subject reduction. I think Mario would say the Coq issues are similar in scope to those Lean in that they aren't a large issue, but should be watched out for. But I think Coq users would counter that they have a plan to fix SR in Coq whereas it is an accepted trait of Lean. I also have the sense that the SR issues in Coq are more compartmentalized to certain Coq features.)
Note: I got a lot of my information from this thread on the Lean Zulip.
The big question of course now is why does Lean have proof irrelevance and syntactic subsingleton elimination if they knowingly lead to these (small) issues? And what big benefits does proof irrelevance and syntactic subsingleton elimination provide to Lean users? I'm trying to figure that out, and then I'll update this answer when I do.
