exactShellAmplitude_zeroPhase
plain-language theorem explainer
At zero phase, the unregulated exact shell amplitude equals the positive real shell mass, viewed in ℂ. Gravity and continuum-blocker arguments cite it to turn real shell-mass lower bounds into complex-norm lower bounds. The proof unfolds the amplitude and mass, then simplifies each summand by exp(0)=1 and the zero phase factor.
Claim. For every natural number $n$, the unregulated exact shell amplitude at the zero phase equals the complex embedding of the real shell mass of shell $n$: $\mathrm{Amp}_{0}(n) = \mathrm{shellMass}(n)$ in $\mathbb{C}$.
background
Module P2-a isolates analytic obligations for removing a complexity cutoff from the phased quotient path sum. Completeness of $\mathbb{C}$ makes Cauchy the exact limit criterion for finite phased sums. The cap-free API packages this as $Z_{\mathrm{cap}}(\mathrm{phase},B)$ (exact quotient shells in range B) and an oscillatory-tail predicate on late contiguous blocks; telescoping equates Cauchy of the cap sequence with that tail criterion.
The exact shell amplitude is the panel-locked, cap-free summand built from ExactPathClass and the same class measure used by shell mass. Zero phase is the constant-zero phase model. Shell mass is the positive real mass of one exact shell (upstream shell scale is $E_{\mathrm{coh}}$ times block capacity). The module stresses that these limits only remove a cutoff: no continuum geometry, mesh refinement, or full-ledger claim.
proof idea
Term-mode proof by unfolding exactShellAmplitude, zeroPhase, and shellMass. Rewrite the real sum as a complex sum via Complex.ofReal_sum. Pointwise Finset.sum_congr reduces each class contribution: the zero phase supplies ofReal 0, multiplication by zero clears the phase angle, Complex.exp_zero gives $1$, and mul_one leaves the real mass term. No external lemmas beyond these arithmetic identities.
why it matters
This identity is the bridge from real shell-mass growth to complex-norm failure of the zero phase. Downstream, zeroPhase_epsilon_one_failure (C1 epsilon-one witness) uses it so that beyond any proposed tail threshold a one-shell block has norm greater than one, via the same ExactPathClass and class measure. zeroPhase_not_exactShellTailCancellation then concludes that zero phase fails ordered-tail cancellation, because positive shell masses grow at least like $n^{3n}$.
In the Seven Gaps story this is the discriminating non-vacuity check: a substrate-derived phase must supply the oscillatory cancellation that zero phase explicitly lacks. It does not itself force a physical phase; it only certifies that the exact-shell criterion is strong enough to reject the trivial model before any continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.