campaign_flags_anchored
plain-language theorem explainer
Five load-bearing increments of the QG seven-gaps campaign are re-derived in one conjunction: nonnegative geometric deficits under every ledger-to-hinge bridge, positive cardinality of each bounded path-sum class, discrete Laplacian eigenvalue convergence on fixed axis modes, vanishing of the n=8 abelian deformation brackets, and the Cayley–Menger non-degeneracy threshold on causal tetrahedra. Gravity auditors cite it to keep the campaign ledger pinned to imported artifacts. The proof is a five-goal refine that applies one named lemma per gap.
Claim. The following five statements hold simultaneously: (1) for every finite recognition ledger $L$ and every ledger-to-hinge bridge $b$, the geometric deficit of $b$ at each comparison point $x_\sigma(i)$ is nonnegative; (2) for every bound $B\in\mathbb{N}$, the scoped bounded complex class has positive finite cardinality; (3) for every fixed mode $k\in\mathbb{N}$, $4N^2\sin^2(\pi k/N)\to(2\pi k)^2$ as $N\to\infty$; (4) on the $n=8$ hypersurface phase space, the deformation bracket of any two generator fields vanishes; (5) for every causal tetrahedron type, edge scale $a>0$, and shear parameter $\alpha$, the Euclidean Cayley–Menger cubic is positive if and only if $\alpha$ exceeds the type-dependent minimum.
background
The Seven-Gaps Campaign Ledger is a machine-checked status record for the quantum-gravity gap campaign, in the style of the QG scope audit. Each gap carries a proved scoped increment and an explicitly open remainder toward full physical closure. This module does not flip any full-strength audit closure flag.
Gap 1 lives in the ledger-bridge no-go: every bridge from a recognition ledger to a hinge geometry forces nonnegative geometric deficits on the image of the comparison map (sign obstruction). Gap 2 is the path-sum measure package: the bounded combinatorial class is finite for each size cap, with a $1/|\mathrm{Aut}|$ measure. Gap 4 is discrete Lichnerowicz: the flat discrete Laplacian eigenvalue identity and its large-$N$ continuum limit, restricted to fixed axis modes. Gap 5 is the abelian momentum sector of hypersurface deformations at period $n=8$ (the eight-tick octave). Gap 6 is the causal-simplex Wick package: Euclidean Cayley–Menger positivity is equivalent to the shear parameter clearing a type-dependent floor.
The shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ appears among the dependency graph edges as the algebraic substrate of recognition cost, though this particular conjunction does not invoke it directly.
proof idea
Term-mode proof by refine ⟨?_, ?_, ?_, ?_, ?_⟩, one subgoal per conjunct.
- Gap 1: introduce the ledger, bridge, and index; apply
bridge_forces_nonneg_geometricDeficit. - Gap 2: apply
PathSumMeasure.boundedComplex_card_posdirectly. - Gap 4: for each mode $k$, rewrite via the discrete-eigenvalue abbreviation and apply
DiscreteLichnerowicz.discreteEigenvalue_tendsto. - Gap 5: introduce generators and a phase-space point; apply
HypersurfaceDeformation.bracket_Dgen_Dgen. - Gap 6: introduce type, scale, and shear with positivity; apply
CausalSimplexWick.cm3_euclidean_pos_iff.
No new analysis is performed here; each flag is re-anchored to its imported kernel lemma so the ledger cannot drift.
why it matters
Without this anchor, the campaign ledger would be a free-floating boolean board. The doc-comment states the design intent: proved flags are re-derived from the imported modules, so status cannot silently diverge from artifacts. Gap 7 is intentionally quarantined and anchored inside the seam-grammar verdict module instead.
Downstream use count is currently zero; the declaration is a ledger integrity theorem rather than a lemma consumed by further physics derivations. It sits at the bookkeeping layer of the gravity seven-gaps campaign and records scoped increments only: substrate-to-triangulation sign no-go, path-sum count-finiteness, axis-mode operator convergence, eight-tick abelian brackets, and causal-class non-degeneracy. Full physical closures (Hessian-symbol match to frozen Regge, continuum path-sum limit, full TT polarization, non-abelian deformation algebra, independent-geometry comparison) remain open, matching the module header's weakest-link tiers.
Framework contact is local to the gravity campaign rather than the T0–T8 forcing chain, though the $n=8$ instance in gap 5 is the same eight-tick octave period forced at T7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.