The Four Tiers
| Tier | Meaning | How to check |
|---|---|---|
| Verified | A theorem in Lean 4 with Mathlib. Zero sorry, zero custom axioms. | Compile the repository, or read the blueprint. |
| Argued | A mathematical or physical argument in a manuscript, not machine-checked. Unrefereed. | Read the manuscript; its assumptions are the points to scrutinize. |
| Conjectural | A proposal or dictionary whose key step is a stated hypothesis. | The hypothesis is named; in the formalization it is carried as an explicit hypothesis, never as an axiom. |
| Empirical | A numerical prediction compared with data. | See the predictions page, including which inputs are fixed. |
Results that are not yet proved are kept in the formalization as named open_ placeholders and counted, so “zero sorry” cannot be mistaken for “everything proved”. Routes that fail are kept as theorems about why they fail.
Status by Research Area
| Area | Status |
|---|---|
| Riemann Hypothesis | Verified in Lean: functional equation, zero pairing, the critical line as the fixed locus of the shadow involution, and exact equivalences between RH and positivity of the Weil form. The Haar-measure L² route is developed in the manuscript; its central step is the next target for formalization. |
| Celestial holography | Verified: shadow transform = time reversal in the model. Central-charge statements carry their physical inputs as explicit hypotheses. Einstein equations from boundary consistency: manuscript. |
| Twistor theory / googly problem | Shadow = T verified; the twistor construction is developed in the manuscript. |
| Yang–Mills mass gap | Shadow = T step verified; the Haar-orthogonality and Kac–Moody steps are developed in the manuscript and are next for formalization. |
| BSD conjecture | Tamagawa/Haar ingredients in progress; known results (Gross–Zagier, Kolyvagin) form the classical background. |
| Quantum foundations | Developed in the manuscript; complex Hilbert space and unitarity from Haar self-duality. |
| Standard Model structure | Division-algebra tower; the three-generation count is the next formalization target. |
| Predictions | Pending experiments, with inputs stated. |
| Philosophy of agency | A formal argument under stated definitions. |
How the Work Is Organized
Results that are not yet proved are kept in the formalization as named open_ placeholders and counted, so “zero sorry” always means no hidden holes, and the open list is public. Routes that fail are kept as theorems about why they fail, so each one is explored once. The manuscripts present the full arguments; the Lean tree records which pieces compile.
Corrections, counter-examples and expert criticism are welcome and are recorded in the open.