A.15 Trust boundary and current verification
On this page · Permalink · Source line 775
The current replay uses Lean 4.34.0-rc2, compiler commit 6a10ac8c22beadecabdbb0919c2b50214762f91d, and Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06. It built the five source modules with warnings treated as errors, printed axiom dependencies for all 96 named theorems, and replayed each module with leanchecker. The compiler and imported dependency cache were not rebuilt from their source. Kernel replay uses Lean's own kernel, not a second independent proof checker.
The axiom union is exactly propext, Classical.choice, and Quot.sound. This is the standard foundation used by the audited proof terms, not an axiom-free claim. The active source contains no proof placeholders, custom axiom declarations, native decision proofs, or unsafe declarations. Historical failed or native-decision drafts are excluded from the active build.
Current source reconciliation checked all five source hashes and all eleven archived check-log hashes against the archived report. All sixteen match. The current inventory contains exactly 96 unique names and 96 archived axiom records. All line numbers agree with the archived source index.
The pinned portable runtime was restored and verified against its combined archive hash. A fresh build, all 96 theorem axiom inspections, and all five kernel replays passed. The complete receipt and logs accompany the source package. Earlier transfer failures remain historical records.