@mildsunrise AFAICT, the approach that this work wants to take follows that of a standard relative consistency proof in mathematical logic: postulate enough inaccessibles+whatever else you want, build a nontrivial "model of Lean" and define an interpretation function of Lean theories (collections of definitions and statements) into the model. Incompleteness does not forbid this and is not the issue.

The unsubstantiated leap is (to oversimplify) to take this "proof" of relative consistency via model existence, and extrapolate that to consistency of the implementation of the Lean kernel. I'm not aware of anyone in the field who seriously doubts the existence of models of "idealized Lean", insofar as such a thing exists separate from its official implementation.