exactShellAmplitude_tick_fiberwise
plain-language theorem explainer
The weighted exact-shell amplitude under a Fin-8 tick phase factors as a sum over the eight tick fibers of fiber mass times the corresponding 8th root of unity. Anyone proving shell-amplitude vanishing from mass balance or antipodal balance cites this regrouping. The proof is a fiberwise Finset split plus constancy of the exponential on each fiber.
Claim. Fix a tick assignment $\tau$ sending each exact path class of complexity $n$ to an element of $\mathrm{Fin}\,8$. The exact-shell amplitude of the derived phase $\theta(c)=2\pi\,\tau(c)/8$ equals $\sum_{p=0}^{7} m_n(p)\,\omega^p$, where $m_n(p)$ is the total class measure on the fiber $\{\,c:\tau(c)=p\,\}$ and $\omega=e^{2\pi i/8}$.
background
This module banks the Wave C1 Gap2 residual R2 schema: exact path classes already quotient by global equivalence, so a map ExactPathClass n → Fin 8 is well-posed on classes. The eight-tick API supplies only a Fin-8 trace hypothesis; equidistribution content is an independent Prop here. Dead constant-phase classes are blocked elsewhere; escape needs intra-shell tick variance.
The exact shell ExactPathClass n is the disjoint union over shell signatures of the global-equivalence quotient of exact labeled complexes of complexity exactly $n$. Each class carries a positive real measure classMu. The tick-derived phase attaches radians $2\pi\cdot\mathrm{tick}/8$ to a class; its complex exponential is the unit 8th root tickRoot of that tick (proved by tickDerivedPhase_exp). Fiber mass is the sum of classMu over classes with a fixed tick.
The shell amplitude is the classMu-weighted sum of $e^{i\theta(c)}$ over the shell. Grouping that sum by tick is the algebraic step that turns balance hypotheses into root-of-unity cancellation.
proof idea
Unfold the amplitude, fiber mass, and fiber definitions. Split the shell sum into eight fibers of $\tau$ via Finset.sum_fiberwise_of_maps_to (maps-to universe). On each fiber $p$, rewrite the exponential by tickDerivedPhase_exp and the filter membership $\tau(c)=p$, so every summand is classMu(c)·tickRoot p. Factor tickRoot p out of the fiber sum (Finset.sum_mul) and cast the real mass sum to $\mathbb{C}$. Congruence over $p$ finishes.
why it matters
This is the regrouping bridge from tick fibers to shell amplitudes in the Gap2 tick-phase substrate. Downstream, exactShellAmplitude_eq_zero_of_massBalanced and the per-shell exactShellAmplitude_eq_zero_of_massBalanced_at rewrite with it, then cancel by equal fiber masses times $\sum_{p}\omega^p=0$. The antipodal bridge exactShellAmplitude_eq_zero_of_antipodalBalanced_at does the same with four opposite-root cancellations under $m(p)=m(p+4)$.
Framework-wise it sits on the eight-tick octave (forcing T7): phase is $2\pi\cdot k/8$, and vanishing is 8th-root orthogonality, not a continuum argument. It feeds ShellAmplitudeVanishes under mass balance, which is necessary for late-block tail cancellation but not sufficient; TypedResidual_strengthened_tick_balance and analytic OscillatoryTail for the signature-vertex witness stay open. It does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.