ShellAmplitudeVanishes
plain-language theorem explainer
The shell-local balance condition: for any phase on exact path classes, the complex amplitude of each exact complexity shell tends to zero as complexity tends to infinity. Cited by anyone using the P2.4 shell-balance blocker or proving necessity of uniform oscillatory tails. Defined as the ordinary ε-N limit of the shell-amplitude norm; no proof content beyond the Prop body.
Claim. A phase assignment on exact path classes of complexity $n$ has vanishing shell amplitudes when, for every $\varepsilon>0$, there exists $N$ such that for all $n\ge N$, the complex norm of the exact-shell amplitude $\sum_c \mu(c)\,e^{i\,\mathrm{phase}(n,c)}$ is strictly less than $\varepsilon$.
background
Module P2.4 isolates the missing phase content in the Zq continuum blocker. Carrier facts already give finite exact shells, positive class masses, large shell mass, and a fixed-cap pairing witness, but no substrate action that resolves phases inside every late shell. Limits are in the complexity cutoff only; they are not mesh refinement and make no geometric-continuum claim.
The exact path class at complexity $n$ is the set of combinatorially distinct exact complexes of that complexity (disjoint union over shell signatures of the quotient by global equivalence; no bounded-complex cap). The exact-shell amplitude is the unregulated phased sum over that class: each class mass times $e^{i\theta}$. The shell scale itself is coherence energy times block capacity, but only the phased sum enters this definition.
Upstream, the oscillatory-tail predicate demands uniform cancellation on contiguous late blocks. This definition records the weakest shell-local consequence of that demand.
proof idea
Definitional, not a proved theorem. The body is the standard sequential limit: for every positive $\varepsilon$ there is a complexity cutoff past which the complex norm of the exact-shell amplitude stays below $\varepsilon$. No tactics, no lemmas applied; the Prop is exactly that $\varepsilon$-$N$ statement in terms of the already-defined exact-shell amplitude.
why it matters
Weakest necessary condition for the P2.4 phase-balance blocker. Downstream, the necessity theorem shows every oscillatory tail forces this vanishing; the shell-constant obstruction shows any phase constant on each shell fails it (norm equals the diverging positive shell mass); the full P2.4 certificate and the ledger pillar theorem package both facts with the finite-repair obstruction. Module doc is explicit: finite-cap pairing and complexity-only phases cannot supply even this local vanishing, so any closing phase must rebalance every late shell. Lands in the Seven Gaps gravity chain as the minimal asymptotic intra-shell balance demand before the stronger uniform block control of the oscillatory tail. No full-theory flag is flipped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.