shellConstant_not_shellAmplitudeVanishes
plain-language theorem explainer
A phase constant on each exact complexity shell cannot drive individual shell amplitudes to zero at large complexity. Anyone citing the P2.4 shell-balance blocker or the complexity-phase no-go needs this intermediate. The proof rewrites the shell-amplitude norm as the positive shell mass and picks a late shell whose mass exceeds one.
Claim. Let $\varphi$ assign a real phase to every exact path class at each complexity $n$. Suppose $\varphi$ is shell-constant: within each fixed $n$, every class receives the same phase. Then the exact-shell amplitudes of $\varphi$ do not tend to zero: it fails that $\forall\varepsilon>0\,\exists N\,\forall n\ge N$, $\|A_n(\varphi)\|<\varepsilon$.
background
Module P2.4 isolates the missing phase input for the Zq continuum blocker. Carrier facts give finite exact shells, positive class masses, and large shell mass, but no substrate action that balances phases inside late shells. Limits are complexity cutoffs, not mesh refinement.
A phase is shell-constant when it ignores class labels inside each exact complexity shell and may still vary arbitrarily with the shell index $n$. The shell-local balance condition (forced by any uniform oscillatory tail) asks that individual exact-shell amplitudes tend to zero as complexity grows. One-shell contiguous blocks reduce exactly to those amplitudes, so the vanishing condition is necessary for an oscillatory tail, though weaker than uniform block control.
For a shell-constant phase the full shell amplitude is the positive shell mass times one common unit phase: no intra-shell cancellation occurs. Shell mass grows with complexity; in particular it exceeds one once $n\ge 2$.
proof idea
Assume shell-amplitude vanishing and instantiate at $\varepsilon=1$ to obtain a cutoff $N$. Set $n=\max(2,N)$. The vanishing hypothesis gives $|A_n|<1$. Rewrite the norm via the shell-constant identity: under shell-constancy, $|A_n|$ equals the exact shell mass at $n$. The mass lower bound for $n\ge 2$ yields mass $>1$, contradicting the strict inequality. Pure term-mode contradiction; no induction.
why it matters
Feeds the complexity-phase no-go: any phase that only sees shell complexity fails the oscillatory-tail obligation, whatever common shell phase it chooses. That no-go is one conjunct of the certified P2.4 blocker certificate, which packages three facts: oscillatory tails force shell-amplitude vanishing; finite-shell repairs (eventually zero phase) cannot produce a tail; and complexity-only phases cannot either.
Together these pin the remaining P2.4 premise as genuine asymptotic intra-shell balance from richer substrate structure, not relabeling invariance, finite-cap pairing, or a complexity-only phase. The module sits in the gravity seven-gaps program and does not alter full-theory flags. Landmark context is the exact-shell UV gauge and the continuum-blocker phase obligation, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.