exactShellAmplitude_eq_zero_of_massBalanced
plain-language theorem explainer
Equal class-mass on the eight tick fibers of a shell forces that shell's exact amplitude to vanish by eighth-root cancellation. Gravity and QG residual work cite it as the algebraic core of the Gap-2 tick-phase bridge. The proof rewrites the amplitude fiberwise, factors a constant mass out of the Fin-8 sum, and applies sum-of-roots vanishing.
Claim. Fix a tick assignment $\tau$ from exact path classes in each shell to $\mathrm{Fin}\,8$. If the eight tick fibers of every shell carry equal $classMu$-mass, then for every shell index $n$ the exact-shell amplitude of the derived phase $2\pi\cdot\tau/8$ is identically zero.
background
This module banks the Wave C1 R2 exact-shell tick-phase enrichment schema for Gap 2. Exact path classes already quotient by the global equivalence on each shell signature, so a map from classes to $\mathrm{Fin},8$ is well-posed. The eight-tick API supplies only a Fin-8 trace hypothesis; equidistribution content is stated here independently.
TickFiberMassBalanced asserts equal $classMu$-mass across the eight tick fibers of each shell. That is the load-bearing bridge hypothesis: pure cardinal equidistribution cannot cancel unequal class masses. The derived phase is $2\pi\cdot\mathrm{tick}/8$, and the shell amplitude is the complex weighted sum of eighth roots of unity against those fiber masses.
The local setting is the Recognition eight-tick octave (period $2^3$), the same Fin-8 structure that appears as the T7 forcing landmark and as the Cl$_8$ grading in the Clifford bridge. Dead classes (shell-constant and eventually-zero phase) are already blocked elsewhere; escape needs genuine intra-shell tick variance.
proof idea
Rewrite the shell amplitude in tick-fiber form via exactShellAmplitude_tick_fiberwise, so the claim is that $\sum_{p:\mathrm{Fin},8} m_n(p),\omega^p=0$ with $m_n(p)$ the fiber mass and $\omega$ a primitive eighth root.
Mass balance gives $m_n(p)=m_n(0)$ for every $p$. Congruence of the sum replaces each mass by the constant $m_n(0)$, then Finset.mul_sum factors it out. The remaining geometric sum $\sum_p \omega^p$ is zero by sum_tickRoots_eq_zero. A final ring step yields $0$.
why it matters
This is the algebraic engine of the Gap-2 tick-phase bridge. The parent bridge theorem tickEquidistribution_implies_shellAmplitudeVanishes packages it into the shell-local necessary condition ShellAmplitudeVanishes: mass-balanced Fin-8 fibers cancel by eighth-root orthogonality.
Two tail-blocker parents reuse the same identity: mass balance implies every exact-shell amplitude vanishes, so contiguous late-block sums of zeros give ExactShellTailCancellation and the panel-locked OscillatoryTail indexing, with no extra estimate.
Framework-wise it realizes the T7 eight-tick octave as a cancellation mechanism inside gravity residuals. It does not close the strengthened contiguous late-block residual, nor the analytic oscillatory tail for the signature-vertex witness (R4), and it does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.