Verification
The complete fresh verification of the reviewed Theorems A and B passed on 13 September 2026. The record concerns the frozen source snapshot described here.
Extended fresh audit — View report · Download evidence
Run Fresh-20260913T121046Z. Final identity check: 17:16:21 UTC. The downloads are separately labelled copies with personal filesystem prefixes replaced. The original evidence remains intact; no new Lean audit was run to prepare this website.
| Check | Recorded result |
|---|---|
| Ordinary project verification | PASS. The earlier 222-source project build reused pinned imported-library artifacts. It remains a separate historical run. |
| Fresh source rebuild | PASS. All 3,399 imported non-toolchain modules rebuilt: 222 project, 2,920 Mathlib and 257 other dependency modules. Source compilation took 219.72 minutes across two sessions. |
| Fresh replay of rebuilt artifacts | PASS. Official leanchecker --fresh, native exit 0, in 17.73 minutes. The replay started from an empty kernel environment. |
| Theorem types and definition identities | PASS. The four real/complex theorem types matched their reviewed propositions without extra premises; 23 reviewed definition bodies were recorded. |
| Transitive axiom inspection | PASS. Raw inspection covered 157 claim records and all 5,683 eligible project declarations. Their only reachable axioms were propext, Classical.choice and Quot.sound. |
| Source and artifact identity | PASS. Four identity checkpoints covered build completion, before replay, after replay and after inspection. |
The source rebuild began with an empty artifact directory. It retained Lean’s pinned compiler, bundled standard libraries, runtime and official checker. The checker uses Lean’s own kernel; this is not verification by an independently implemented kernel. The compiler was not bootstrapped. The build used native Lean directly; a complete standalone Lake build, optional style linters and Lake cache hooks were outside the run.
The official checker’s unsafe and partial declarations are excluded from replay and separately inventoried. All 18 project exclusions were verified as compiler-generated recursion companions. The imported environment contains other axiom declarations, but none beyond the three listed above is reachable from the checked project declarations. No project-origin axiom was introduced.
The saved report records the recovered Windows status-writer interruption and the initial widget-launcher failure. There were no failed native Lean module attempts; the actual native exits and recovery records are preserved.
Statements and scope
| Proved declaration | Exact proposition |
|---|---|
PL1.theoremAReal | PL1.TheoremARealStatement |
PL1.theoremAComplexStrong | PL1.TheoremAComplexStrongStatement |
PL1.theoremBReal | PL1.TheoremBRealStatement |
PL1.theoremBComplexStrong | PL1.TheoremBComplexStrongStatement |
The generic declarations PL1.theoremA and PL1.theoremB are also proved. Every clause of each specification concerns one projection and its actual range. Real and complex witnesses, and the witnesses for A and B, need not be identified.
The complex endpoints prove that the underlying real range has no equivalent real lattice norm. This mathematically implies the complex Banach-lattice conclusion in the paper. The general bridge to a complex Banach-lattice definition is not separately formalised in this project.
All four reviewed A/B targets are proved. Further geometry and the remaining scope of the frozen development are recorded in its inventory. Those geometric results concern their specified constructed spaces and norms; they are not silently attached to an arbitrary witness of A or B.
Full theorem inventory · README and proof-route account · Theorem B’s formal proof route
The formal argument for B uses a direct complemented-lattice alternative and an arbitrary-copy exclusion proved from the concrete construction. Establishing the principal theorem by this route does not verify every intermediate step in a different manuscript proof.
Checking correspondence with the paper is a separate mathematical judgement from kernel checking. The saved A semantic review and B semantic review document the formalisation’s comparisons; they are not independent third-party certification or a record of final author sign-off.
The audit and its inventory identify the original formal source and manuscript snapshot. The paper currently available here retains the same Theorem A and Theorem B statements. Updating the manuscript does not rerun the Lean audit.
Source and dependencies
Inspect all 222 frozen Lean modules · Download source and dependency pins
The displayed excerpts are extracted from these source files. Their full imports, section parameters, namespaces and proofs are available in the source views. Excerpts are not claimed to compile independently of that context.
- Lean
4.34.0-rc2, revision6a10ac8c22beadecabdbb0919c2b50214762f91d. - Mathlib revision
4cbb42e75a050e830b7cf0f2ae748d7644f59cf7. - BanLat upstream revision
5c9360ccd9cef27b749f3cabda6348fd2529d1a3. Its 21 reused source files retain the documented compatibility port and Apache 2.0 attribution.
Library provenance · BanLat licence · All dependency pins
The source archive contains the mathematical development and pinned configuration. The evidence archive is supporting evidence, not a standalone reconstruction of the entire audit environment: compiled artifacts, dependency trees and all per-module logs remain outside that download. The bundle explains its scope and keeps references to the historical originals.
Evidence and provenance
Read the evidence-bundle notes · Machine-readable facts · Original and prepared evidence hashes · Download hashes and sizes · Complete served-file manifest
Original report SHA-256: 292329105fe246fed4bc5fd97a4dde7272d0531fe2d2408e3ef50c9632e3bdc7. Historical hashes identify the original bytes; prepared-copy hashes identify the downloads. Hashes bind files to a recorded snapshot and are not an external certificate of mathematical truth.
Acknowledgement
The project-specific Lean development was produced by ChatGPT in Codex with minor supervision by Antonio Acuaviva, who permitted alternative proofs where more efficient to formalise while retaining the intended statements. Imported libraries retain their own authorship and attribution.