Reproducible Lean build

The Lean development is checked by compiling its 38 modules. A successful compilation means that the Lean kernel accepted every proof of every formal statement. It does not by itself show that a formal statement matches the English sentence it is linked to; that correspondence is reviewed in each claim record.

Pinned toolchain

• Lean 4.26.0 (leanprover/lean4:v4.26.0, commit d8204c9fd894f91bbb2cdfec5912ec8196fd8562)
• Mathlib v4.26.0, commit 2df2f0150c275ad53cb3c90f7c98ec15a56a1a67, pinned in lean/phase8/lakefile.toml and lake-manifest.json. Only RealNoise and RealFourier import Mathlib; the other 36 modules use Lean core and Std only.

Commands

From the root of this edition's source folder (the folder that contains lean/ and tools/):

# 1. Pinned Mathlib, needed only for RealNoise and RealFourier (downloads into lean/phase8/.lake)
cd lean/phase8
lake exe cache get        # optional: official build cache, where the network allows it
lake build Mathlib.Data.Real.Archimedean Mathlib.Data.Fintype.BigOperators Mathlib.Algebra.BigOperators.Fin \
  Mathlib.Algebra.Order.BigOperators.Group.Finset Mathlib.Tactic.Linarith Mathlib.Tactic.Positivity \
  Mathlib.Tactic.FieldSimp Mathlib.Tactic.NormNum Mathlib.Tactic.Ring Mathlib.Tactic.GCongr
cd ../..

# 2. Compile all 38 modules into a NEW directory (the script refuses to reuse one)
sh tools/lean/build_bundle.sh work/lean_build_$(date +%Y%m%d_%H%M%S) lean/phase8

# 3. Summarise the run: exit codes, warnings and every #print axioms report
python3 tools/lean/parse_build.py work/lean_build_<stamp> work/lean_build_<stamp>.json

# 4. (site maintainers) export declaration types and dependencies for the website
LEAN_PATH="$(cd lean/phase8 && lake env printenv LEAN_PATH):$PWD/work/lean_build_<stamp>/olean" \
  lean tools/lean/ExportDecls.lean      # writes data/lean_export.json

The per-phase scripts lean/phase*/build.sh from the original deliveries are included unchanged; they write build products inside the source tree, so the bundle script above is preferred.

Fresh build recorded for this edition

Run in a new, isolated output directory (lean_fresh_20261010), Lean (version 4.26.0, x86_64-unknown-linux-gnu, commit d8204c9fd894f91bbb2cdfec5912ec8196fd8562, Release). Started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z. Result: 38 of 38 modules compiled; 1588 axiom reports, one for each audited theorem, using only (none); propext; propext, Classical.choice, Quot.sound; propext, Quot.sound; 126 linter warnings (unused simp arguments and variables), no errors, no sorry. Machine-readable summary: summary.json.

Independent audit (dated evidence)

The development was independently audited on 2026-10-10: "Independent phase-8 audit and manuscript connections". The audit report, its declaration index and its correspondence map are reproduced unchanged in evidence/audit/. They are dated evidence from that audit, not results of this site build.

Rebuilding the website

cd tools && npm ci && cd ..     # KaTeX 0.16.11 (pinned in tools/package.json)
python3 tools/build_site.py         # regenerates dist/ from the manuscript, content and data
python3 tools/validate_site.py      # fidelity, link, anchor and browser checks
python3 tools/serve.py              # local preview