tickFiber
plain-language theorem explainer
Inside exact shell n, the fiber over a Fin-8 tick residue p is the set of exact path classes whose assigned tick equals p. Anyone proving shell equidistribution, fiber mass balance, or eighth-root cancellation of shell amplitudes cites this set. The body is a plain universe filter on the tick assignment.
Claim. Given a tick assignment $\tau$ sending each exact path class in shell $n$ to a residue in $\{0,\ldots,7\}$, the tick fiber over $p$ is $\{ c \in \mathrm{ExactPathClass}(n) : \tau_n(c) = p \}$.
background
This module banks the Wave C1 Gap2 residual R2 schema: exact path classes already sit in the GlobalEquivalent quotient of shell signatures, so a map from classes to Fin 8 is well-posed by construction. The eight-tick API is only a Fin-8 trace hypothesis; it does not supply equidistribution. Escape from the dead classes ShellConstant and EventuallyZeroPhase needs genuine intra-shell tick variance.
The fundamental RS time quantum is one tick ($\tau_0 = 1$), and one octave is eight ticks (forcing-chain T7). Here the tick assignment is combinatorial data on path classes, not the continuum time unit. Shell scale elsewhere is $E_{\mathrm{coh}}$ times block capacity; this definition only partitions classes inside a fixed shell index $n$.
Downstream mass and amplitude statements sum or count over these fibers. The non-circular guard compares only fiber cardinalities and never mentions amplitudes, oscillatory tails, or limits.
proof idea
Definition, not a proof. The body is Finset.univ.filter retaining those exact path classes $c$ in shell $n$ with $\tau_n(c)=p$. No lemmas are applied.
why it matters
This fiber is the combinatorial substrate for the Gap2 tick-phase enrichment. TickEquidistributedInShell is equality of fiber cardinalities across all eight residues. tickFiberMass sums class weights over the fiber; constant-mu plus card equidistribution yields mass balance, which feeds the root-of-unity bridge that cancels shell amplitude via eighth-root orthogonality.
Parent uses include the fiberwise regrouping of exact shell amplitude, the succ and antipodal ($+4$) mass-preservation bridges under tail fiber shifts, and the shell-zero mass blocker. Framework landmark: T7 eight-tick octave. The module still leaves open strengthened late-block tail cancellation and analytic OscillatoryTail for the signature-vertex witness; this definition only names the fibers those arguments partition over. It does not flip gap2 continuum-and-measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.