tickRoot
plain-language theorem explainer
Defines the unit eighth-root character of a discrete tick: for each residue class p in Fin 8, the complex value exp(2πi p/8). Downstream Gap2 lemmas cite it as the phase weight on tick fibers when proving shell-amplitude cancellation by root-of-unity orthogonality and antipodal pairing. The body is the standard complex exponential; no proof content.
Claim. For each tick index $p \in \{0,1,\ldots,7\}$, the unit eighth-root character is $\omega_p := \exp(2\pi i\, p/8) \in \mathbb{C}$.
background
This module banks the Wave C1 R2 exact-shell tick-phase enrichment schema for the Gap2 residual. Exact path classes already carry a well-posed Fin-8 tick assignment; dead classes (shell-constant and eventually-zero phase) are blocked upstream, so escape needs genuine intra-shell tick variance.
The eight-tick structure (Recognition landmark T7: period $2^3$) appears here only as a Fin-8 trace. Equidistribution is an independent Prop on fiber cardinalities inside each shell, not supplied by the EightTick hypothesis. Shell amplitudes are complex sums of phase weights over those fibers.
tickRoot is the elementary character that turns a tick label into that phase weight. Sibling notions (derived phase $2\pi\cdot\mathrm{tick}/8$, tick fibers, fiber mass, mass-balanced fibers) all evaluate against this character when cancelling amplitudes.
proof idea
Pure definition: unfold to the complex exponential $\exp(2\pi i, p/8)$ with $p$ coerced from Fin 8 through naturals into $\mathbb{C}$. No lemmas, tactics, or hypotheses.
why it matters
Parent results in Gap2AntipodalBalanceBridge use this character as the phase factor on fiber masses. Opposite ticks negate: $\omega_{p+4}=-\omega_p$, so equal antipodal masses cancel pairwise and force exact shell amplitude zero without Q-independence. The same weights appear in posting-history continuum bridges as the character pushforward (fiberwise history amplitude equals class measure times the tick root).
Framework landmark: T7 eight-tick octave. The sum of all eight roots vanishes, which is the algebraic engine behind mass-balanced fiber cancellation and ShellAmplitudeVanishes. The module still leaves open contiguous late-block tail cancellation and the analytic oscillatory tail for the signature-vertex witness; this definition only supplies the character those arguments need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.