p24_shell_balance_blocker_certificate
plain-language theorem explainer
Packages the P2.4 shell-balance blocker: any uniform oscillatory tail forces per-shell amplitudes to vanish, while finite-support and shell-constant phases cannot produce such a tail. Gravity ledger authors cite it to mark the continuum phase gap as sharp. The proof is a three-way conjunction of already-proved no-go lemmas.
Claim. For every assignment of real phases to exact complexity-$n$ path classes: (i) a uniform oscillatory tail (late contiguous shell-amplitude blocks arbitrarily small) implies that individual shell amplitudes tend to zero; (ii) any phase that agrees with the zero phase outside finitely many shells fails the oscillatory-tail condition; (iii) any phase constant on each shell (possibly depending on $n$) likewise fails the oscillatory-tail condition.
background
In the Seven Gaps gravity program, exact complexity shells are the sets ExactPathClass n: combinatorially distinct exact complexes of complexity exactly $n$, with no bounded-cap truncation. A phase assigns a real number to each class in each shell. The shell amplitude is the phased sum over that shell; its norm tracks residual mass after intra-shell interference.
The continuum blocker demands an OscillatoryTail: for every $\varepsilon>0$ there is $N$ so that every contiguous block of shell amplitudes with both endpoints $\ge N$ has norm $<\varepsilon$. No rate or summability is assumed. Limits are in the complexity cutoff only, not mesh refinement.
This module isolates what that tail forces and what cannot supply it. ShellAmplitudeVanishes is the weakest shell-local necessary condition (each late shell amplitude $\to 0$). EventuallyZeroPhase is the abstract shape of any finite-cap repair (phase eventually zero). ShellConstant means the phase does not distinguish classes inside a shell, so no intra-shell cancellation occurs and the amplitude norm equals the positive shell mass.
proof idea
Term-mode triple pairing. The certificate is literally
⟨oscillatoryTail_implies_shellAmplitudeVanishes, eventuallyZeroPhase_not_oscillatoryTail, shellConstant_not_oscillatoryTail⟩.
The first lemma reduces a one-shell contiguous block to the shell amplitude, so uniform block control yields per-shell vanishing. The second is the finite-cap no-go: eventual agreement with the zero phase inherits the zero phase's failure of the tail (late blocks still see the large residual shell mass). The third uses that a shell-constant phase has shell amplitude equal to shell mass times a unit phase factor, hence non-vanishing late amplitudes and no oscillatory tail.
why it matters
Closes the certified P2.4 blocker in the Seven Gaps ledger. Downstream, gap2_shell_balance_blocker_certified re-exports the same conjunction as the Pillar 2 shell-balance blocker: the remaining OscillatoryTail obligation is sharp, so any closing phase must rebalance every late shell.
The module doc states the residual open content explicitly: carrier facts give finite exact shells, positive class masses, large shell mass, and a fixed-cap pairing witness, but not a substrate action that resolves phases inside every late shell. Neither relabeling invariance, finite-cap pairing, nor complexity-only phases supply the missing asymptotic intra-shell balance.
In the broader Recognition gravity stack this keeps the continuum/phase gap honest: no full-theory flag flips, and the eight-tick or continuum phase symbols appearing in imports are not used to claim geometric continuum cancellation here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.