one_shell_block
plain-language theorem explainer
The sum of exact-shell amplitudes over the single-shell window $[n,n+1)$ equals the amplitude of shell $n$ alone. Anyone reducing uniform late-block cancellation to per-shell vanishing cites this identity. The proof is three Finset rewrites: Ico-as-difference, range successor, left cancellation.
Claim. For any real phase assignment on exact path classes of each complexity $n\in\mathbb{N}$, the contiguous one-shell block sum equals the shell amplitude: $\sum_{k\in[n,n+1)} A(\mathrm{phase},k)=A(\mathrm{phase},n)$, where $A$ is the exact-shell amplitude functional.
background
Module P2.4 isolates the missing phase-balance input for the $Z_q$ continuum blocker. Carrier facts already give finite exact shells and positive shell masses; they do not supply a substrate action that cancels phases inside every late shell. The weakest shell-local necessary condition is that individual late exact-shell amplitudes tend to zero; the stronger uniform condition is cancellation on every late contiguous block (the oscillatory-tail property).
An exact path class at complexity $n$ is the disjoint union, over shell signatures, of quotients of exact labeled complexes by global equivalence: no bounded-cap type appears. The exact-shell amplitude of a phase assignment is the coherent sum of $e^{i\theta}$ over those classes at fixed $n$. Contiguous block sums are ordinary Finset sums of those amplitudes over half-open integer intervals.
This lemma records the trivial one-shell case of that block sum, so that the uniform tail hypothesis can be specialized to single shells without extra analysis.
proof idea
Pure Finset arithmetic, no phase content. Rewrite the half-open sum $\sum_{k\in\mathrm{Ico},n,(n+1)}$ as the difference of two range sums via sum_Ico_eq_sub, using $n\le n+1$. Expand the upper range by sum_range_succ, then cancel the common lower partial sum with add_sub_cancel_left. The remaining term is exactly the amplitude at $n$.
why it matters
Parent theorem: oscillatoryTail_implies_shellAmplitudeVanishes (Necessary Balance Theorem). That result obtains an $N$ from the oscillatory-tail hypothesis at tolerance $\varepsilon$, then applies the one-shell identity to each $k\ge N$ so that the single-shell amplitude is itself a late contiguous block and hence smaller than $\varepsilon$. Without this reduction, uniform block control would not formally imply the weaker per-shell vanishing condition stated in the module doc.
In the Seven Gaps ledger this closes the elementary bridge from P2.4's strong tail obligation down to ShellAmplitudeVanishes. It does not invent balance: it only makes the specialization rigorous. Framework context is the gravity-side continuum blocker, not the T0–T8 forcing chain; limits are complexity cutoffs, not mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.