Pillar2Closed
plain-language theorem explainer
Pillar 2 of the full quantum-gravity campaign is closed exactly when two benchmark flags are true: the substrate-to-geometry bridge is derived, and the path-sum measure admits a continuum limit. Anyone tracking the QG full-theory ledger cites this as the second conjunct of the master closure criterion. The body is a two-conjunct boolean equality on the benchmark record.
Claim. Given a full-theory benchmark record $b$, Pillar 2 is closed if and only if both $b$'s bridge-derived flag and $b$'s continuum-and-measure flag equal $\mathrm{true}$. Equivalently: the substrate-to-geometry bridge is derived and validated, and the Recognition path-sum has a proved continuum limit on the simplicial class with a substrate-derived measure.
background
This module is the Phase 0c full-theory ledger for the quantum-gravity campaign. It records one boolean per pillar benchmark; a flag may flip to true only after the named target theorem is kernel-checked, axiom-audited, and critic-passed. The three pillars are classical recovery to Einstein gravity, a well-defined quantum amplitude, and at least one confirmed discriminating prediction.
Pillar 2 is the quantum-amplitude pillar. Its first flag (gap1) licenses a derived substrate-to-geometry bridge, targeting recognition_ratio_derived together with independent geometry checks (signed Regge deficit witness and ledger-Hessian equality to the Regge-Dirichlet form at $N=5$). Its second flag (gap2) licenses Z_RS_continuum_limit on the simplicial class with a substrate-derived path-sum measure.
The ambient structure FullTheoryBenchmarks packages these flags so the closure criterion cannot drift from the machine-checked targets. The ledger is anchored to the seven-gaps campaign starting line and cannot contradict that record.
proof idea
Definitional abbreviation, not a proved theorem. The proposition is the conjunction of two boolean equalities on fields of the benchmark structure: bridge-derived equals true, and continuum-and-measure equals true. No tactics or lemmas are invoked; downstream theorems simply unfold this definition and simplify against the concrete starting-line record.
why it matters
This is the middle conjunct of FullTheoryClosed, the master closure criterion: the full theory in the strongest sense is closed exactly when all three pillars are closed. It is also the middle conjunct negated in all_pillars_open, which records that each pillar is individually open at the starting line.
In the campaign plan, Pillar 2 is the well-defined quantum amplitude: derived bridge plus path-sum measure with proved continuum limit. Closing it would discharge the quantum side of the full-theory claim, complementary to classical Einstein recovery (Pillar 1) and a discriminating prediction such as the alpha band or BMV witness (Pillar 3). Until both gap1 and gap2 flip, the honest gate full_theory_not_yet_closed remains provable and blocks any premature closure claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.