exactShellAmplitude_shellConstant
plain-language theorem explainer
For a phase constant on each exact complexity shell, the shell amplitude factors as the positive shell mass times one common unit complex phase; no intra-shell cancellation occurs. Gravity workers on the Seven Gaps P2.4 phase-balance blocker cite this factorization. The proof unfolds the amplitude as a finite sum of class masses, factors the shared phase via sum-mul, and applies shell-constancy pointwise.
Claim. Let $\varphi$ assign a real phase to every exact path class of complexity $n$. Suppose $\varphi$ is shell-constant: on each shell $n$ it takes the same value on every class as on a fixed isolated class. Then the exact shell amplitude equals $(\mathrm{shell\ mass}\,n)\cdot\exp(i\,\varphi_n(\mathrm{isolated\ class}))$ in $\mathbb{C}$.
background
Module setting is Seven Gaps P2.4: the phase obligation inside OscillatoryTail for the Zq continuum blocker, attacked without assuming cancellation. Carrier facts already give finite exact shells, positive class masses, and large shell mass; they do not supply a substrate action that resolves phases inside every late shell.
An exact path class at complexity $n$ is a combinatorially distinct exact complex of that complexity (disjoint union over shell signatures of the quotient by global equivalence). The shell amplitude sums, over those classes, each class mass times a unit complex phase $e^{i\varphi}$. Shell mass is the total positive real mass of the shell.
Shell-constancy means the phase does not distinguish classes inside any fixed shell: it may still vary arbitrarily with the complexity index $n$, but on each shell it equals its value on one isolated class.
proof idea
Term-mode algebraic factorization. Unfold the shell amplitude and the shell-mass definition so the left-hand side is a finite sum of real class masses converted to $\mathbb{C}$ and multiplied by unit phases. Rewrite the real sum as a complex sum and factor the common complex exponential out of the sum via Finset.sum_mul. Pointwise, shell-constancy replaces each class phase by the isolated-class phase, so every summand carries the same unit factor and the remaining real sum is exactly the shell mass.
why it matters
This is the structural identity behind the shell-constant blocker. Its sole downstream consumer is the norm theorem: the complex norm of a shell-constant amplitude equals the (diverging, positive) shell mass exactly. That norm identity is what feeds shellConstant_not_oscillatoryTail: a complexity-only phase, constant inside each shell, cannot drive late shell amplitudes to zero, so it cannot witness the oscillatory tail.
In the module's logic chain, finite-cap pairing and relabeling invariance are already ruled out as insufficient; this result closes the remaining naive escape (assign one phase per shell). The missing P2.4 input must therefore be genuine asymptotic intra-shell balance, at least shell-amplitude vanishing and in fact the stronger contiguous-block control of the oscillatory tail. Limits here are complexity cutoffs only, not mesh refinement or geometric continuum claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.