8.3. Pins and trust boundary🔗

Proof: Lean v4.33.1, mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Comparator: 2312244ac716564a61cc0bf4e107d9abf1757a61. Exporter: 15f6055e299ad5b89345e533cc2192f4cc00f659, built with the proof toolchain. Only propext, Quot.sound, and Classical.choice are allowed as proof axioms.

Documentation: Lean v4.35.0-rc2, Verso 9f8096e40b31715b1d8d5997f15a0bd832f7e37d. SubVerso: d047cb484b2f3598187450935dbcc84d078cb581 in both projects. The proof project exports the checked Lean terms and their types. Verso reads this data to build the hover information.

The contributor guide explains how to build, audit, and extend the checked development. The original mathematical reference presents the classical method. Our written derivation makes the boundary limit direction and the convergence arguments explicit.