tickFiberMass_shell_zero
plain-language theorem explainer
On shell 0, for any Fin-8 tick assignment, the tick-fiber mass at phase p equals the unique class measure if that class is assigned to p, and zero otherwise. Gravity/gap-2 authors cite this as the finite-head concentration fact behind all-shell mass-balance impossibility. The proof unfolds the fiber sum, rewrites the shell-0 universe as a singleton, and splits on the phase equality.
Claim. For every tick assignment $\tau$ (sending each exact path class on shell $n$ to a phase in $\mathrm{Fin}\,8$) and every phase $p\in\mathrm{Fin}\,8$, the tick-fiber mass of shell $0$ at $p$ equals $\mu(c_0)$ if $\tau(0,c_0)=p$, and equals $0$ otherwise, where $c_0$ is the unique exact path class on shell $0$ and $\mu$ is the per-class measure.
background
This module hardens the R4 residual in the Gap-2 tick-phase story: all-shell tick-fiber mass balance would force every exact-shell amplitude to vanish (hence contiguous-block cancellation and an oscillatory tail), but shell 0 is a singleton class, so positive class measure cannot be equidistributed across eight ticks.
Exact path classes on shell $n$ carry a positive per-class measure $\mathrm{classMu}$. A tick assignment $\tau$ labels each class by a phase in $\mathrm{Fin},8$. The tick-fiber mass at shell $n$ and phase $p$ is the sum of $\mathrm{classMu}$ over classes on that shell mapped to $p$. Upstream, shell 0 is known to be a singleton (universe of exact path classes is a singleton finset), with unique representative $\mathrm{isolatedClass},0$.
The local setting is Wave C1 R4: finite-head impossibility of all-shell balance, plus an eventual-balance repair that makes late amplitudes vanish so the finite head does not obstruct oscillatory-tail statements.
proof idea
Unfold the definitions of tick-fiber mass and the underlying fiber filter. Rewrite the universe of exact path classes on shell 0 via the sibling fact that it is a singleton finset, then apply Finset.filter_singleton. Split on whether the unique class is assigned to phase $p$: both branches simplify to the claimed conditional (the class measure, or zero).
why it matters
This is the concrete concentration identity used by the design-named packaging theorem that shell 0 is a subsingleton and that some single fiber carries all of its class measure while the other seven are empty. That packaging feeds no_tickFiberMassBalanced: there is no Fin-8 tick assignment mass-balanced on every shell, because shell 0 always dumps positive measure into one fiber and leaves another empty (via fin8_add_one_ne).
In the Gap-2 residual DAG this is clause (b) of the R4 hardening: finite-head impossibility of all-shell TickFiberMassBalanced. It does not close the open R4 residual (existence of a substrate phase with oscillatory tail escaping dead classes), nor the signature-level blocker target, and it does not flip gap2_continuum_and_measure. The eight-tick octave (T7) is the phase set being unbalanced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.