exactShellAmplitude_congr
plain-language theorem explainer
Exact shell amplitudes coincide whenever two phase assignments agree on every path class of a fixed complexity shell. Gravity and continuum-blocker arguments cite this to transport shell-amplitude and oscillatory-tail statements between eventually agreeing phases. The proof unfolds the finite phased sum and rewrites each summand by the pointwise hypothesis.
Claim. Let $\varphi$ and $\psi$ assign a real phase to every exact path class of complexity $n$. If $\varphi_n(c)=\psi_n(c)$ for all classes $c$ at that shell, then the unregulated shell amplitudes agree: $\sum_c \mu(c)\,e^{i\varphi_n(c)}=\sum_c \mu(c)\,e^{i\psi_n(c)}$ in $\mathbb{C}$.
background
The module isolates the missing phase-balance input for Seven Gaps P2.4. Carrier facts already give finite exact shells, positive class masses, and large shell mass, but no substrate action that resolves phases inside every late shell. The weakest shell-local necessary condition is that late exact-shell amplitudes tend to zero; the stronger uniform contiguous-block control is the oscillatory-tail predicate.
An exact path class at complexity $n$ is a combinatorially distinct exact complex of that complexity: the disjoint union over shell signatures of the quotient of the exact labeled class by global equivalence, with no bounded-complex cap in the type. The unregulated shell amplitude of a phase assignment is the finite complex sum $\sum_c \mu(c),e^{i,\mathrm{phase}_n(c)}$ over those classes, with $\mu(c)$ the class mass.
This congruence is the shell-local rewriting step that lets tail statements move between two phase functions once they agree on all classes of a given shell.
proof idea
Unfold the definition of the unregulated shell amplitude to a finite sum over exact path classes. Apply Finset.sum_congr with a reflexive index equality, then rewrite each summand by the pointwise phase hypothesis on that class. No cancellation, mass estimates, or limit arguments enter.
why it matters
Parent use is oscillatoryTail_of_eventuallyAgrees: one direction of tail transport along eventual phase agreement. That theorem obtains a cutoff from eventual agreement, then needs shell amplitudes (and contiguous blocks) to match for all larger shells; this congruence supplies the per-shell equality.
In the P2.4 blocker narrative, the point is negative: finite-cap pairing, relabeling invariance, and complexity-only phases do not yield asymptotic intra-shell balance. Congruence under full shellwise phase agreement is the legitimate transport tool, not a substitute for balance. Limits here are complexity cutoffs only; they make no mesh-refinement or geometric-continuum claim, and no full-theory flag moves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.