9.4. Trust boundary🔗

Appendix A.2 of Zheng (2026) states the scope of the verification, and every clause of it is checkable against the pinned repository. The appendix is running prose — it numbers no result — so this section quotes it verbatim rather than restating it as a formal environment, and then says what stands outside it. The paper's words, from the paragraphs titled Scope and logical foundations of the verification (Zheng, 2026, Section A.2):

The formal verification is end-to-end. Theorem A.1 is universally quantified over H and r and derives both directions of the equivalence. The development includes proofs of the stress–codimension inequality for collinearity flags, the minimal-prime height theorem for the Split–Klein isotropic-difference ideal, and the exclusion of exceptional pin parameters; none is assumed by Theorem A.1.

The project introduces no custom mathematical axioms. It does not use sorry, admit, explicit opaque declarations, or an external oracle in place of any mathematical argument. Nor do the structure fields of the flag states or function-field branches contain the stress–codimension or height conclusions to be proved. The project theorems and the mathlib theorems they invoke are all checked by the Lean kernel.

The foundational axiom dependencies of the final theorem are exactly propext, Classical.choice, Quot.sound. These are, respectively, propositional extensionality, classical choice, and the compatibility principle for quotient types. Here “unconditional” means that Theorem A.1 is a closed proposition: H and r are bound by universal quantifiers, and no additional mathematical hypotheses or project-specific axioms occur. The verification uses Lean 4.29.0; the corresponding mathlib commit is 8a178386ffc0f5fef0b77738bb5449d50efeea95. The accompanying toolchain file and dependency manifest pin these two versions.

The quotation reflows the appendix's two displayed lines — the three axiom names and the mathlib commit — into the sentences that introduce them, and changes nothing else.

The appendix describes the formalization as it stood at the release the paper accompanies. The pinned commit has since moved on, and two further closed roots now stand beside Theorem A.1: the partition criterion in Euclidean local-rigidity form, and the same criterion for continuous motions. Every clause quoted above remains true of Theorem A.1, and the toolchain and mathlib commit the appendix names are still the ones the pin records. What the appendix does not describe is the passage those two roots cross, from attained maximum rank to rigidity in the Euclidean sense, which the paper cites and the formalization has since proved.

The three axioms are the ones nearly all of mathlib depends on: propositional extensionality, classical choice, and quotient soundness. The formalization repository checks the closure itself, in test modules that run #print axioms on each of the three roots, and this blueprint's build resolves every declaration it names against that same pinned commit. The closure was also collected here, directly from the kernel environment at the pinned commit: all three roots depend on exactly those three axioms and on nothing else.

Three things stand outside the kernel check. The classical statement the paper cites for the step from maximum rank to rigidity has no Lean counterpart in the form it is cited: neither its rank formula nor its measure-zero complement is proved. The step itself is proved, by an equivalence of the formalization's own, so what stands outside is the paper's route to it rather than the conclusion. Whether the formal statements say what the paper's theorem says is a reading question no kernel can settle; the statement chapter exists so that a reader can settle it, definition by definition. And the check itself trusts the Lean kernel and the toolchain it runs on, a trust base the verification shares with every Lean development at these versions.

Two parts of the formalization repository stand outside this accounting, both by choice. Challenge.lean and Solution.lean are the statement and proof halves that Comparator expects; the challenge file carries a deliberate sorry, which the proof library neither imports nor contains. And interop/combinatorial-rigidity/ is a separate Lake package, on its own toolchain, proving that this development's rigidity ranks agree with those of CombinatorialRigidity, a library by the author of this blueprint. No file outside that directory names it, so no root theorem depends on it.