norm_exactShellAmplitude_shellConstant
plain-language theorem explainer
For any phase constant on each exact complexity shell, the complex norm of the shell amplitude equals the positive shell mass. Seven-gaps gravity workers cite this when excluding complexity-only phases as sources of late-shell cancellation. The proof rewrites the amplitude as mass times a common unit exponential and applies standard complex-norm identities.
Claim. Let a phase assign a real number to each exact path class at complexity $n$. If the phase is shell-constant (the same value on every class inside each fixed-$n$ shell), then for every $n\in\mathbb{N}$, $\|A_n\| = m_n$, where $A_n$ is the exact-shell amplitude and $m_n>0$ is the shell mass at complexity $n$.
background
Module P2.4 isolates the missing phase-balance input for the Zq continuum blocker. Carrier facts already give finite exact shells, positive class masses, and large shell mass, but no substrate action that cancels phases inside late shells. The weakest shell-local necessary condition is that every late exact-shell amplitude tends to zero; the stronger uniform condition is an oscillatory tail on contiguous blocks.
A phase is shell-constant when it does not distinguish classes inside any exact complexity shell, though it may still vary arbitrarily with complexity $n$. Under that hypothesis the full shell amplitude collapses to the positive shell mass times one common unit complex phase, so no intra-shell cancellation can occur.
Shell mass is the positive real weight of the exact shell at complexity $n$ (built from class masses). Exact-shell amplitude is the complex sum of those masses times $e^{i\theta}$ over classes in the shell. Limits here are complexity cutoffs only, not mesh refinement or geometric continuum claims.
proof idea
Term-mode rewrite chain. First apply the sibling identity that a shell-constant phase makes the exact-shell amplitude equal to $\mathrm{shellMass},n$ times $\exp(i\theta_n)$ for the common shell phase. Then use multiplicativity of the complex norm, identify the real factor's norm with absolute value, drop the absolute value via positivity of shell mass, and cancel the unit modulus of $\exp(i\theta)$. The last step is multiplication by one.
why it matters
This is the quantitative engine behind shellConstant_not_shellAmplitudeVanishes: if the phase is shell-constant, the shell-amplitude norm equals the diverging positive shell mass, so the amplitude cannot tend to zero and even the weakest shell-local balance condition fails. Module doc states the broader blocker: neither relabeling invariance, finite-cap pairing, nor a complexity-only phase supplies the missing P2.4 input; genuine asymptotic intra-shell balance is required.
In the Seven Gaps gravity program this closes one concrete escape route on the path toward the oscillatory-tail obligation in the Zq continuum blocker. It does not itself force the continuum claim; it only shows that shell-constant phases are insufficient. Framework context is discrete complexity shells and phase sums, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.