H12 formal companion
The canonical tree contains one byte-authenticated selected copy of each mathematical module (42 modules, 453 distinct theorem declarations). The v0.14 current block is a subset of 25 theorem declarations: 11 new and 14 unchanged inherited. Counts are not added across repeated archive versions. Compiler acceptance certifies the exact types and their explicit hypotheses; it does not prove the original gamma/class-field equality.
Use H12_Cubic_Divisor_Lean_Guide.pdf for the scope and declaration guide. DECLARATION_INVENTORY.json contains names, signatures, source lines, origins/hashes, and fresh compiler-expanded theorem types. SOURCE_MODULE_MAP.json maps every selected module and all its historical occurrences. CLAIM_COVERAGE.json records the component-level relationship to the traditional manuscript.
Pinned compiler: Lean 4.34.0-rc2, commit 6a10ac8c22beadecabdbb0919c2b50214762f91d. Pinned Mathlib: aeb72f1e9981b6d35b426b16dca7759be3e7ba06. The current block uses bundled Std only.
python3 verify.py --lean /path/to/pinned/bin/lean --scope current
lake update
lake exe cache get
python3 verify.py --lean /path/to/pinned/bin/lean \
--mathlib .lake/packages/mathlib --scope all \
--memory-mib 3072 --timeout 300 --audit-strategy auto
The verifier builds fresh project objects in a temporary directory, compiles sequentially with one worker and warnings as errors, checks admissions/custom axioms, hashes inputs before and after, prints exact theorem types and transitive axioms, and verifies positive/false arithmetic controls. Full replay uses per-module axiom auditors to avoid one large all-import process. The auto strategy chooses the exact-source-prefix auditor for H12PhaseRegulator and import-based auditors elsewhere. It records each process's exact argv, wall/CPU bounds, actual CPU time, and kernel-reported peak resident memory via POSIX wait4. The heap threshold is distinct from an OS address-space limit. The producing environment's executable-self-location adapter is explained under verification/runtime; normal installations do not need it.
Initial memory-limited attempts and any timeout/retry are retained separately, not erased or silently called successful. The final replay ledger selects only complete compiler-and-axiom evidence with matching source hashes. The single all-import auditor/combined import did not complete at the tested 3072 MiB cap; this is separate from the successful module-scoped evidence. Runtime and Mathlib caches are not included in the publication package.
Four payloads named in a foundation v0.2 historical replay receipt were not preserved, so those old output claims are unverified. Original archive/source authentication and the independent fresh checks are separate evidence.
The recorded final ledger combines the full module-scoped attempt with two focused, disjoint retries. Reproduce the focused retries separately if needed:
python3 verify.py --lean /path/to/pinned/bin/lean --mathlib .lake/packages/mathlib \
--scope all --only H12CMNormCertificate --memory-mib 3072 --timeout 300 \
--audit-strategy module --log-dir verification/retry_cmn_300sec
python3 verify.py --lean /path/to/pinned/bin/lean --mathlib .lake/packages/mathlib \
--scope all --only H12PhaseRegulator --memory-mib 3072 --timeout 300 \
--audit-strategy source --log-dir verification/retry_phase_source_prefix
FINAL_REPLAY_AUDIT.json is the exact union ledger for the recorded executions. The portable auto orchestration is a convenience for replaying the same established per-module commands; no fresh run of that entire auto orchestration is claimed.