What Lean checked
Original independent audit: PASS · 5 September 2026, 23:29 UTC
The main real theorem and the four further theorems below were accepted under the pinned Lean and Mathlib versions. The audit rebuilt all 193 project library modules and checked the theorems’ axioms, placeholders, source integrity, and the main theorem’s transitive dependency graph.
This summary records the preserved 5 September audit. All 233 original source and configuration hashes were rechecked when assembling the companion.
| Lean / Lake | 4.34.0-rc2 / 5.0.0-src+6a10ac8 |
|---|---|
| Mathlib revision | 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 |
| Clean project rebuild | PASS · 177 root-closure + 16 supplementary modules · final build exit codes 0 |
| Executable placeholders | 0 sorry · 0 admit · 0 sorryAx in the scanned source scope |
| Project mathematical axioms | 0 in the audited dependency chain |
| Axioms of each theorem | propext, Classical.choice, Quot.sound |
| Audit scope | 234 local Lean files scanned, including four audit helpers; 2,573 imported ComplementedSubspace declarations axiom-audited |
| Main theorem traversal | 40,291 declarations · 1,332,580 edges · complete traversal, no missing bodies or constants |
| Source preservation | 233 original Lean/configuration hashes unchanged |
| Separate fresh kernel replay | Not part of the original audit. See the extended fresh audit below for replay of the imported logical declarations. |
| Archive reproduction | Source hashes and reproduction instructions are available. A separate rebuild from an extracted archive is not recorded here. |
The certificate establishes that the stored Lean theorem was accepted by the stated kernel under pinned dependencies, without a placeholder or project-defined mathematical axiom in its audited dependency chain. It does not by itself establish that the proposition faithfully translates the paper. That correspondence is documented on the Results and Definitions pages for human inspection.
Public copy SHA256: 89e3f091f56c718a0b87599c6bd9ec95566b97dfdcc4c93639a36f75a9a73928
Original certificate SHA256: 5ee6b720af87fb151af8c7bda3ca525eb1fe3de6226f2f19edd41e9e5b02ec4f
Extended fresh audit — View report · Download evidence · public copy · Public archive SHA256
PASS · 6 September 2026 · Snapshot 875e2219bcfe. Pinned source reproduction, fresh kernel replay including imports, and theorem/axiom checks passed. The pinned Lean toolchain was retained.
The verified declarations
Every declaration below is closed: it takes no unproved mathematical assumptions as parameters. All names are in the namespace ComplementedSubspace.
theorem realMainTheorem : RealMainTheoremStatementFull proof sourceRecorded axiom listMathematical statement ↗
theorem realCorollary : RealCorollaryStatementFull proof sourceRecorded axiom listMathematical statement ↗
theorem realUnconditionalCorollary : UnconditionalCorollaryStatement ℝFull proof sourceRecorded axiom listMathematical statement ↗
theorem realSeparableNonprimarity : SeparableNonprimarityStatementFull proof sourceRecorded axiom listMathematical statement ↗
theorem complexCorollary : ComplexCorollaryStatementFull proof sourceRecorded axiom listMathematical statement ↗
Public evidence copies
Personal computer paths and account names have been removed from these separately labelled copies. The author retains the original evidence unchanged. The proofs and recorded audit conclusions are unchanged; this preparation is not a new Lean audit.
Hashes inside historical reports identify the original files. The public-copy manifests below give both original and new hashes, including archive members. Paths in audit scripts are placeholders to configure before use.
About the public copiesOriginal and public file hashesArchive member hashesCurrent website file hashesCompanion’s 233-file source recheckDetailed build scopeExternal dependency provenance
Source & reproducibility
0.61 MB · Public copy
Public copy SHA256: 55571e0a3e1aafef6b4f78ca946ad7e7158fc6b2c3459232a85ba75bd6e9d4de
Original archive SHA256: 5fc920bc7bb22592c2170ac72447af563d17ef261e7f39dfd6123ba04b074148
8.86 MB · Public copy
Public copy SHA256: 8915f0b4d68d26335b8652c6416847e8ae85fae4f17581d6cb433cdfbdb1ce77
Original archive SHA256: 83c339ca7cd48f6b89de7a8d2b7f85e527a5fd94144686c1980bdc700437ec25
For the portable 177-module proof build, follow BUILDING.md from the verified-source ZIP. To reproduce the full 193-module audit and its dependency graphs, follow README.md from the independent-audit ZIP; the audit scripts need the Lean installation and save locations specified for your computer.
Use the pinned toolchain and Lake manifest with the source archive. The full audit archive includes the audit scripts, source snapshots, reproduction instructions, and full dependency graphs. The original certificate records the precise rebuild commands and scope.
The original 5 September audit rebuilt local project modules while retaining external dependency caches. It did not rebuild Lean or Mathlib from scratch. The enclosing repository had no project commit; source identity is recorded by hashes and archives.
Proof correspondence
Parts of the manuscript’s sphere/Gaussian presentation are replaced by finite frames and explicit finite-sign moment estimates. The formal complex argument uses a real equivalence of the constructed ranges to transfer the established DPR obstructions. The development’s architecture README gives the full account.
Uses Mathlib and vendored BanLat; upstream credits and licences are preserved in the source archive.
Historical audit-helper failures
Two intermediate helper failures are preserved: an unsupported pretty-printer option, and an incorrectly resolved liftIO in the dependency tracer. The audit helpers were corrected and rerun successfully. These were failed helper runs, not missing proofs in the main theorem.
Attribution & methodology
The Lean development was produced entirely by ChatGPT in Codex, with minor supervision by the author. At the author’s request, alternative proofs were permitted where more efficient to formalise, to reduce token usage and formalisation overhead, while retaining the intended mathematical statements.