TickEquidistributedInShell
plain-language theorem explainer
Equal Finset cardinalities of the eight tick fibers inside every exact path shell, for a given tick assignment on exact path classes. Gravity and QG authors cite it as the non-circular combinatorial guard before mass balance or shell-amplitude vanishing. It is a pure Prop definition: no proof, only the equal-card statement in terms of fiber Finsets.
Claim. A tick assignment $\tau$ (sending each exact path class at shell level $n$ to a residue in $\{0,\ldots,7\}$) is equidistributed in shells when, for every $n$ and every pair of residues $p,q$, the fiber of classes mapped to $p$ has the same Finset cardinality as the fiber mapped to $q$.
background
This module banks the Wave C1 R2 residual: enrich exact path classes by an eight-tick phase without smuggling amplitude or tail language into the guard. Exact path classes already quotient by the global equivalence on shell signatures, so a map from classes to $\mathrm{Fin},8$ is well-posed on the nose.
The eight-tick API elsewhere is only a $\mathrm{Fin},8$ trace hypothesis; it does not prove equidistribution. Here equidistribution is an independent proposition. A tick fiber at shell $n$ and residue $p$ is the Finset of exact path classes sent to $p$ by $\tau$. The fundamental RS tick is the time quantum $\tau_0=1$, and one octave is eight ticks (forcing-chain T7).
Per-class measure classMu lives upstream on exact shells and is positive on every class. Mass of a fiber is built from that measure; the present definition deliberately uses only cardinality, never mass, amplitude, oscillatory tails, or limits.
proof idea
No proof: this is a definitional Prop. The body is the universal quantification that, for every shell index $n$ and every pair of residues $p,q\in\mathrm{Fin},8$, the Finset cardinalities of the two tick fibers agree. Downstream lemmas treat the Prop as a hypothesis and transport it to mass balance when classMu is shellwise constant.
why it matters
It is the non-circular combinatorial guard named in the module: equal fiber sizes inside each shell, with no mention of exact shell amplitude, oscillatory tails, or limits. Downstream, cardinal equidistribution plus shellwise-constant class measure yields tick-fiber mass balance; under mass balance, every shell amplitude vanishes by eighth-root orthogonality.
That bridge is the escape from the dead classes (shell-constant and eventually-zero phase) banked in the Zq shell-balance blocker: intra-shell tick variance is required, and equal fiber cards are the clean combinatorial half of the cancellation story. Framework landmark: the eight-tick octave (T7, period $2^3$).
It does not close the strengthened contiguous late-block residual, nor the analytic oscillatory-tail witness (R4), and it does not flip the continuum-and-measure gap flag. Per-shell equidistribution is necessary but not sufficient for uniform block cancellation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.