FullTheoryBenchmarks
plain-language theorem explainer
A seven-flag boolean ledger that records which full quantum-gravity campaign benchmarks are kernel-checked. Each flag names a concrete target theorem (bridge derivation, continuum measure, Lorentzian lift, operator/constraint/action recovery, or a discriminating prediction). Gravity and QG auditors cite it as the single source of truth for pillar closure. It is a pure structure definition: no proof body.
Claim. A record type with seven boolean fields: (1) substrate-to-geometry bridge derived and geometry-validated; (2) continuum limit of the RS path sum on the simplicial class with a substrate-derived measure; (3) 4D Lorentzian lift of the action; (4) discrete stress-tensor spectrum converges on curved backgrounds with quasinormal modes; (5) Dirac algebra continuum limit plus Hojman pinning of GR; (6) edge stress-tensor decomposition with $S_{\mathrm{RS}}\to$ Einstein–Hilbert in 4D; (7) at least one discriminating prediction (BMV entanglement witness or seam effective-count) confirmed.
background
The Full Theory Ledger is Phase 0c of the 2026-07-15 quantum-gravity campaign. It extends the seven-gaps CampaignLedger with a machine-checked status record: zero sorry, zero new axioms. A flag may flip to true only when its named target theorem is kernel-checked, axiom-audited, and critic-passed.
The campaign organizes "full theory in the strongest sense" into three pillars. Pillar 1 is classical recovery at action, operator, and constraint strength in the 4D Lorentzian continuum. Pillar 2 is a derived substrate-to-geometry bridge plus a path-sum measure with proved continuum limit. Pillar 3 is at least one confirmed discriminating prediction (BMV entanglement or alpha effective-seam closure).
Upstream anchors include the forced spatial dimension $D=3$ from the T-chain, BIT kernel families for continuum kernels, and simplicial face maps used in discrete geometry. The ledger re-derives the campaign starting-line OPEN flags so it cannot contradict the record it extends.
proof idea
No proof: this is a structure declaration. Each field is a Bool annotated with the exact theorem name whose existence licenses flipping it (for example recognition_ratio_derived and the Regge/Hessian witnesses for the bridge flag; S_RS_converges_EH_4d for action recovery). Downstream, a concrete inhabitant fullTheoryBenchmarks assigns the live truth values, and the pillar-closure predicates read those fields by equality to true.
why it matters
This structure is the type of the live benchmark state and of every pillar-closure predicate. Pillar1Closed requires action, operator, constraint, and Lorentzian flags; Pillar2Closed requires bridge and continuum/measure; Pillar3Closed requires the discriminating prediction. FullTheoryClosed is their conjunction, so the eventual closure claim cannot drift from the flags.
The master theorem full_theory_not_yet_closed stays provable until every pillar flips; when a target theorem lands, only the corresponding field in the inhabitant changes. Framework landmarks in play are the continuum limit of the RS action toward Einstein–Hilbert, the $D=3$ spatial setting, and the path-sum measure on the recognition substrate. The open gate is pillar 3 (theory-maker) together with still-false classical and quantum flags in the current inhabitant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.