sevenGapsCampaignStatus
plain-language theorem explainer
Canonical boolean ledger for the 2026-07 QG seven-gaps campaign: each gap records a proved increment and an explicit OPEN remainder toward full physical closure. Gravity auditors and full-theory ledger modules cite it as the machine-checked starting line. The body is a pure structure instance with literal true flags; no proof obligations.
Claim. The seven-gaps campaign status record sets, for gaps 1--7, the proved-increment flags and the remaining-open flags all to true: gap 1 has sign/parity no-gos and a quadratic energy bridge proved, Hessian-symbol comparison open; gap 2 has count-finiteness and $1/|\mathrm{Aut}|$ measure proved, continuum limit open; gap 3 has proper conformal subspace and shear witness proved, full TT decomposition open; gap 4 has flat TT convergence proved, curved QNM open; gap 5 has lattice Dirac relations proved, continuum HKT algebra open; gap 6 has kinematical Wick certified, action continuation open; gap 7 has seam-grammar miss certified, true mechanism open.
background
The Seven-Gaps Campaign Ledger is a machine-checked status record for a scoped quantum-gravity campaign, in the style of the QG scope audit. It intentionally does not flip any full-strength closure flag: those record complete physical closures, and none of the campaign increments is full-strength.
The structure SevenGapsCampaignStatus holds one proved/open flag pair per gap. Gap 1 (substrate-to-triangulation) covers sign and parity no-gos against raw-deficit bridges, plus a coboundary-strain J-ledger energy bridge with quadratic matching; the Hessian-symbol comparison to frozen Regge remains open. Gap 2 (path-sum measure) covers count-finiteness and the relabeling-invariant $1/|\mathrm{Aut}|$ measure with unit-modulus partition-function bound; continuum limit is open. Gap 3 (tensor sector) proves the conformal image is proper on the $N=5$ Freudenthal torus with an explicit non-conformal shear witness; full TT decomposition is open. Gaps 4--7 similarly split discrete/operator, lattice Dirac, kinematical Wick, and seam-grammar increments from their continuum or mechanism remainders.
Imported modules (LedgerBridgeNoGo, LedgerEnergyBridge, PathSumMeasure, EdgeTensorSector, DiscreteLichnerowicz, HypersurfaceDeformation, CausalSimplexWick) supply the kernel-checked increments that the flags summarize.
proof idea
Pure definitional instance: each field of the status structure is assigned the Boolean literal true. There is no tactic proof, no lemma application, and no computation beyond structure construction. The values encode the campaign's self-reported outcome (every gap has both a proved scoped increment and an explicit open remainder).
why it matters
This record is the single machine-checked starting line for later gravity ledgers. Downstream, no_full_physical_closure_claimed reads every OPEN bit and asserts that the campaign does not claim full physical closure. FullTheoryLedger.starting_line_anchored re-derives the same open bits so the full-theory ledger cannot drift from the campaign baseline.
Terminal guards and binding receipts for individual gaps consult these flags when a later close is claimed: Gap4's curved/QNM open bit must clear while flat TT convergence stays proved; Gap5's continuum HKT open bit must clear with constraint-recovery terminals; Gap6's action-continuation open bit must clear while kinematical Wick stays certified (V2 Lorentzian action path). Wick-action hinge and lookalike-receipt status theorems likewise pin their flags to this ledger.
In the Recognition gravity stack the ledger enforces weakest-link honesty: scoped increments (no-gos, finite path-sum measure, proper conformal subspace, discrete Lichnerowicz convergence, lattice Dirac, kinematical Wick) are recorded without overclaiming continuum, curved-QNM, full TT, or true seam-mechanism closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.