tickEquidistribution_implies_shellAmplitudeVanishes
plain-language theorem explainer
Mass-balanced Fin-8 tick fibers force every exact-shell amplitude of the derived eighth-root phase to vanish. Gap-2 residual and gravity workers cite this as the combinatorial-to-analytic bridge from tick equidistribution to the shell-local necessary condition. The proof rewrites each shell amplitude to zero by eighth-root orthogonality under equal fiber mass, then takes the zero threshold in the vanishing predicate.
Claim. Let $\tau$ assign to each exact path class an element of $\mathrm{Fin}\,8$. If the eight tick fibers of every shell carry equal $\mathrm{classMu}$-mass (mass balance), then the shell amplitudes of the derived phase $2\pi\cdot\tau/8$ all vanish: for every $\varepsilon>0$ there is $N$ such that for all $n\ge N$, the exact-shell amplitude at $n$ has complex norm strictly less than $\varepsilon$.
background
This module banks the Wave C1 R2 schema residual: enrich exact shells by a Fin-8 tick assignment on ExactPathClass n (already a GlobalEquivalent quotient), derive the phase $2\pi\cdot\mathrm{tick}/8$, and escape the dead classes ShellConstant and EventuallyZeroPhase that live in the Zq shell-balance blocker. The eight-tick API supplies only a Fin-8 trace hypothesis; equidistribution content is an independent Prop here.
Two guards sit upstream of the bridge. Cardinal equidistribution demands equal fiber cardinalities inside each shell and never mentions amplitudes or tails. Mass balance strengthens that to equal classMu-mass across the eight fibers; the doc notes that cardinal equidistribution alone cannot cancel unequal class masses. With shellwise-constant classMu, the cardinal guard transports to mass balance.
The derived phase is the eighth-root character on the tick label. Shell amplitude is the mass-weighted sum of those roots over a shell; vanishing of those amplitudes is the shell-local necessary condition for later oscillatory-tail control. The fundamental tick is the RS time quantum ($\tau_0=1$), and one octave is eight ticks (T7).
proof idea
Tactic proof, short. Unfold ShellAmplitudeVanishes by introducing $\varepsilon>0$. Supply threshold $N=0$ via refine, so the claim is pointwise for every shell index $n$. Rewrite the exact-shell amplitude at $n$ by the sibling lemma that mass-balanced fibers cancel under eighth-root orthogonality (exactShellAmplitude_eq_zero_of_massBalanced), then apply norm_zero so the norm is $0$, which is $<\varepsilon$. No induction and no tail estimates: pure per-shell cancellation.
why it matters
Fills the named design bridge in the Gap-2 hard-core plan: mass-balanced Fin-8 fibers cancel by 8th-root orthogonality and yield the shell-local necessary condition. Module doc lists it among the proved theorems of the R2 enrichment schema, alongside the substrate structure, the non-circular cardinal guard, and the signature-vertex witness that escapes both dead classes.
It sits on the eight-tick octave (T7): the phase is $2\pi\cdot k/8$, and cancellation is the geometric sum of eighth roots of unity. Downstream, the contiguous late-block residual remains OPEN: per-shell vanishing is necessary but not sufficient for uniform smallness of every contiguous late block sum (ExactShellTailCancellation / OscillatoryTail). The banked reverse implication is one-directional. Closing that R3→R4 analytic half is the next scaffold; this theorem does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.