This file is a concise guide to what the public AST Lean subset currently establishes and what it still records as explicit bridge or assumption structure.
Theorem: proved directly in the canonical public modules.Bridge: represented canonically, but still depends on an explicit interpretation or external mathematical bridge.Open: planned but not yet closed in the public canonical tree.
Theorem: finite involution substrate and boundary/interior partition in Level0.leanTheorem:Dist(C) = 2^{|σBdry(C)|}/K = log Diststructural package in Level0.leanTheorem: discreteKspectrum,log 2gap, and closed-region minimum in Level0.leanTheorem: correction-step monotonicity and iterate nonincrease in Level1_Correction.leanTheorem: beta-flow fixed-point structure in Level1_BetaFlow.lean
Theorem: Boolean event-logic exclusion in Level2_QuantumResults.leanTheorem: orthomodularity from SCEP in Level2_QuantumResults.leanTheorem: multiplicative-to-power closure and direct quadratic Born rule in Level2_QuantumResults.leanBridge: Hilbert-space and Born-rule emergence packages are represented in Level2_QuantumBridge.leanBridge: manifold/spacetime emergence is represented canonically in Level2_ManifoldBridge.lean and Level2_SpacetimeBridge.lean, with the established classical route bundled in Level2_GeometryRoute.lean and an internal Hurwitz-basedd = 3support path packaged in Level2_ManifoldBridge.leanBridge: inflation interpretation formulas are represented in Level2_InflationBridge.lean
Bridge: GR large-scale limit and Lovelock route in Level3_GRBridge.lean and Level3_GeometryRoute.leanTheorem: LQG kinematical comparison package in Level3_LQG.leanTheorem: tensor-mode counting used by the inflation paper in Level3_TensorModes.leanTheorem: soliton/worldsheet kinematics in Level3_Soliton.leanTheorem: Hurwitz / no-fifth-force package in Level3_Hurwitz.lean including the internal quaternion-imaginary-basis3-support
Theorem: holographic entropy package H1-H6 and Newton-constant matching in Holography.leanTheorem: corrected fine-structure denominator1/α = 4πσ_min - log 2 - 1/2, corrected positivity, and tight corrected window in AlphaEstimate.leanBridge: inflation observables package in Inflation.leanTheorem: proton-stability package in ProtonStability.lean, now explicitly linked to the Hurwitz/Fanoσ_min = 11count
Open: internal manifold/spacetime emergence without explicit bridge recordsOpen: fulld = 3and GR closure without the current geometric bridgesOpen: inflation pivot derivation and complete tensor-ratio closureOpen: 4D central-charge closure for the string paperOpen: subleading correction that closes the remaining fine-structure gap
The large-scale geometry route is best read as a staged chain, not as a single all-or-nothing theorem.
| Step | Current status | Lean home | Notes |
|---|---|---|---|
β = 1 shell/growth control |
Theorem |
Level1_BetaFlow.lean and the promoted geometry bridge layer | This is the AST-side rate/growth input. |
| polynomial-growth to manifold emergence | Bridge |
Level2_ManifoldBridge.lean | This currently depends on the classical Gromov/Kleiner polynomial-growth bridge. |
strict Huygens to d = 3 |
Bridge |
Level2_SpacetimeBridge.lean | This currently depends on the classical Hadamard-Gunther theorem together with the AST-to-Huygens bridge. |
internal Hurwitz support for d = 3 |
Theorem |
Level3_Hurwitz.lean and Level2_ManifoldBridge.lean | This gives an internal quaternion-based 3-support path alongside the classical bridge route. |
GR uniqueness in 3+1 dimensions |
Bridge |
Level3_GRBridge.lean | This currently depends on Lovelock as a cited classical theorem after the manifold and dimension bridges are in place. |
The bridge steps above are not placeholders for unknown AST mathematics. They are explicit interfaces to established external mathematical theorems.