exactShellAmplitude
plain-language theorem explainer
Defines the complex amplitude of one exact-complexity shell: sum over path classes of class measure times a unit-modulus phase factor. Gravity and continuum-blocker arguments cite it as the atomic shell contribution inside capped path sums and tail estimates. The body is a direct finite sum, not a derived identity.
Claim. Given a real phase assignment on exact path classes at each complexity level $n$, the exact-shell amplitude at $n$ is the complex number $\sum_{c} \mu(c)\, e^{i\,\theta_n(c)}$, where the sum runs over exact path classes of complexity $n$, $\mu(c)$ is the class measure, and $\theta_n(c)$ is the assigned phase.
background
This module isolates analytic obligations for removing a complexity cutoff from a phased quotient path sum. Finite capped sums are complete in $\mathbb{C}$ precisely when they are Cauchy; the exact-shell API packages that criterion as uniform smallness of late contiguous shell blocks (an oscillatory tail), not as mesh refinement or continuum geometry.
An exact path class is a nonduplicating quotient shell at fixed complexity index $n$. The class measure supplies the real weight of each class. A phase model assigns a real number to every class at every $n$; the corresponding complex weight is the unit-modulus factor $e^{i\theta}$.
The eight-tick phase ladder ($k\pi/4$ for $k=0,\ldots,7$) appears downstream when phases are tick-derived. Upstream shell and interface constructions fix the discrete carrier; this definition only packages one shell's phased sum.
proof idea
Definitional: expand as the finite sum over ExactPathClass n of (classMu c : ℂ) times Complex.exp (I * phase n c). No lemmas, no tactics, no rewriting. Downstream proofs rewrite with this definition, then cancel fiberwise (e.g. antipodal Fin 8 pairs) or telescope into capped cutoffs.
why it matters
This is the atomic shell term for the panel-locked complexity cutoff. Downstream, the cap-shell bridge identifies the sum of shells through $B$ with the exact complexity cutoff. Antipodal-balance bridges prove that tick-fiber mass balance forces each shell amplitude to vanish by four opposite-root cancellations, hence eventual balance yields an oscillatory tail on the tick-derived phase.
Enriched-carrier and posting-history residual arguments reuse the same amplitude: identical-zero shells close the bare R5 tail shape, and posting-history amplitudes are matched against this exact-shell form. In the Recognition gravity stack this is the cancellation primitive a substrate-derived phase must supply so the phased $Z_q$ sequence can drop its complexity cap (Seven Gaps P2-a). It does not itself force the eight-tick octave or $D=3$; those enter only when the phase is specialized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.