SevenGapsCampaignStatus
plain-language theorem explainer
Boolean status record for the 2026-07 quantum-gravity seven-gaps campaign: one proved/open flag pair per gap. Auditors and higher ledgers cite it as the typed campaign surface. Pure structure definition with no proof obligation; the concrete snapshot is the sibling value that fills the flags.
Claim. A record type of boolean fields, one pair (or triple) per gap $1$--$7$: whether the campaign proved each scoped increment (sign/parity no-gos, quadratic energy bridge, path-sum count finiteness and $1/|\mathrm{Aut}|$ measure, proper conformal subspace with shear witness, flat TT eigenvalue convergence on the AXIS stencil, lattice Dirac relations, kinematical Wick certification, seam-grammar certified miss) and whether the residual full-strength closure (Hessian-symbol comparison, continuum limit, full TT decomposition, curved QNM, continuum HKT algebra, action continuation, true mechanism) remains open.
background
The module is a machine-checked campaign ledger in the style of the QG scope audit. It records scoped increments from the imported SevenGaps modules without flipping any full-strength audit closure flag: none of the increments is a full physical closure.
Gap 1 concerns the substrate-to-triangulation map: the ledger-bridge no-go module gives sign and parity obstruction theorems against a raw-deficit bridge form; the energy-bridge module builds the corrected coboundary-strain J-ledger with two-sided quadratic matching. Gap 2 is the path-sum measure (count-finiteness, relabeling quotient, $1/|\mathrm{Aut}|$ weights). Gap 3 is the edge-tensor conformal sector on 3D triangulations. Gap 4 is discrete Lichnerowicz / flat TT operator convergence (AXIS stencil only). Gaps 5--7 cover lattice Dirac relations, kinematical Wick rotation, and the seam-grammar miss.
Upstream constants such as the RS-native $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ appear only as ambient gravity infrastructure; this structure itself carries no numeric physics.
proof idea
No proof. The declaration is a Lean structure whose fields are boolean status bits, some annotated with doc-comments that scope the proved claim (for example gap 4 is flat TT eigenvalue convergence on the AXIS stencil sector only, not isotropic flat-space recovery). Instantiation is deferred to the sibling definition that fills each flag.
why it matters
Gives a single typed surface for the campaign outcome. The only direct consumer is the concrete value that sets the flags (gap-1 no-gos and quadratic bridge true; Hessian comparison open; gap-2 count and measure true; continuum limit open; and so on through gap 7). Downstream readers can pattern-match on proved versus open without re-reading seven modules.
In the Recognition gravity stack this is bookkeeping, not a forcing-chain step: it does not touch T5--T8, RCL, or the mass ladder. Its role is honesty about weakest-link tiers toward full QG closure, keeping scoped kernel-checked increments separate from full-strength audit flags. Open residuals named in the fields (Hessian-symbol comparison, continuum path-sum limit, full TT decomposition, curved QNMs, continuum HKT algebra, action continuation, true seam mechanism) are the live research targets the ledger tracks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.