Pillar1Closed
plain-language theorem explainer
Pillar 1 (classical recovery) is closed exactly when four benchmark flags are true: action recovery, operator recovery, constraint-algebra recovery, and 4D Lorentzian action. Anyone tracking the full-theory campaign ledger cites this as the packaging of those flags. The body is a pure definitional conjunction on a FullTheoryBenchmarks record; no proof work.
Claim. For a full-theory benchmark record $b$, pillar 1 (classical recovery to Einstein gravity in the 4D Lorentzian continuum, at action, operator, and constraint strengths) is closed if and only if the action-recovery, operator-recovery, constraint-recovery, and Lorentzian-action flags of $b$ are all true.
background
This module is the live benchmark ledger for the full quantum-gravity theory campaign. Status is machine-checked: zero sorry, zero new axioms. One boolean per pillar benchmark; a flag may flip to true only when its target theorem is kernel-checked, axiom-audited, and critic-passed. The three pillars are classical recovery, a well-defined quantum amplitude (derived bridge plus path-sum continuum limit), and at least one confirmed discriminating prediction.
FullTheoryBenchmarks is the structure holding those flags. Every field documents the exact target theorem whose existence licenses flipping it. Pillar 1, per the module doc, is classical recovery at all three strengths (action, operator, constraint algebra) to Einstein gravity in the 4D Lorentzian continuum limit. The four flags conjoined here are exactly that package: gap action recovery, gap-4 operator recovery, gap-5 constraint recovery, and gap-6 Lorentzian action.
The ledger re-anchors the seven-gaps campaign starting line so full-theory flags cannot contradict the campaign record they extend.
proof idea
Definitional, not a proved theorem. The predicate is the four-way conjunction that the named Bool fields of the benchmark record equal true. No lemmas, no tactics, no reduction beyond structure-field projection and Boolean equality.
why it matters
This is the first conjunct in the master closure criterion: full theory closed means pillar 1, pillar 2, and pillar 3 are all closed. Downstream, FullTheoryClosed is literally that triple conjunction, and all_pillars_open proves each pillar (including this one) fails on the starting-line benchmark record. The master gate full_theory_not_yet_closed stays provable until every pillar flips; because closure is definitional in these flags, the eventual claim cannot drift from the ledger.
In the Recognition gravity program this packages the classical limit of the discrete recognition substrate: recovering Einstein gravity as continuum action, operator content, and constraint algebra, with a 4D Lorentzian lift. It does not itself discharge the seven-gaps blockers; it only names when those classical-recovery targets count as done for campaign bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.