all_pillars_open
plain-language theorem explainer
At the full-theory campaign starting line, none of the three pillars is closed: classical recovery, quantum amplitude (bridge plus measure), and a confirmed discriminating prediction. Campaign auditors cite this as the machine-checked open baseline that the ledger must not drift from. The proof is a three-branch contradiction by simplifying the starting benchmark flags to false.
Claim. On the starting-line full-theory benchmark record, pillar 1 is not closed (classical recovery fails at least one of action, operator, constraint algebra, or 4D Lorentzian action), pillar 2 is not closed (derived substrate-to-geometry bridge and continuum path-sum measure are not both certified), and pillar 3 is not closed (no confirmed discriminating prediction flag).
background
The Full Theory Ledger is Phase 0c of the quantum-gravity full-theory campaign. It holds one boolean flag per pillar benchmark; a flag becomes true only after the target theorem is kernel-checked, axiom-audited, and critic-passed. Closure of the full theory in the strongest sense is the conjunction of three pillars.
Pillar 1 is classical recovery at all three strengths (action, operator, constraint algebra) to Einstein gravity in the 4D Lorentzian continuum, plus a Lorentzian action flag. Pillar 2 is a derived substrate-to-geometry bridge together with a path-sum measure that has a proved continuum limit. Pillar 3 is at least one confirmed discriminating prediction (BMV entanglement witness or alpha effective-seam closure).
The module imports the seven-gaps CampaignLedger and re-derives the OPEN starting line, so this ledger cannot contradict the machine-checked campaign record it extends. The master status theorem that the full theory is not yet closed remains provable until every pillar flag flips.
proof idea
Term-mode proof via refine into a triple of implications, each discharging one negated pillar-closed claim by contradiction.
For pillar 1, project the operator-recovery conjunct from the assumed closed record and simp against the concrete starting fullTheoryBenchmarks value (that flag is false). For pillar 2, project the bridge-derived conjunct and simplify the same way. For pillar 3, unfold the single-flag closed predicate and simplify the discriminating-prediction flag to false. No external lemmas beyond the in-module benchmark constant and the three pillar predicates.
why it matters
This is the per-pillar open baseline for the full-theory campaign ledger. It pins the starting state that full_theory_not_yet_closed and the closure criterion FullTheoryClosed are measured against: the master theorem stays provable until every pillar flips, and the closure definition cannot drift from the flags.
Downstream the ledger is meant to track progress on classical recovery (action, operator, constraint algebra, Lorentzian continuum), the quantum amplitude (substrate bridge plus convergent path-sum measure), and at least one discriminating prediction. Anchoring to the imported CampaignLedger keeps the full-theory module synchronized with the seven-gaps OPEN record.
In the broader Recognition framework this is campaign infrastructure rather than a forcing-chain step (T5–T8, RCL, phi). It records that the strongest full-theory claim is still open at the audited start line, without asserting any new physics identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.