tickDerivedPhase
plain-language theorem explainer
Converts a Fin-8 tick label on each exact path class into a real phase in radians via 2π·k/8. Gravity Gap-2 residual work cites it whenever shell amplitudes, antipodal fiber balance, or oscillatory tails are stated on a tick-derived phase. The body is a pure definitional map; no proof content.
Claim. Given a tick assignment $\tau$ that sends each exact path class of complexity $n$ to an element of $\{0,\ldots,7\}$, the derived phase is the map $\theta_n(c) = 2\pi \cdot \tau(n,c)/8$ (radians).
background
This module banks the Wave C1 R2 exact-shell tick-phase enrichment schema for Gap 2. Exact path classes of complexity $n$ are the GlobalEquivalent quotient of exact labeled complexes (disjoint union over shell signatures); a tick assignment on those classes is therefore well-posed by construction.
The eight-tick octave (period $2^3$) is the Recognition landmark T7: ticks live in $\mathrm{Fin},8$, and the natural unit character is the 8th root of unity. The fundamental RS time quantum is one tick ($\tau_0=1$ in RS-native units), but here "tick" means the discrete $\mathrm{Fin},8$ label on a class, not the real time constant.
Dead residual classes (shell-constant phase, eventually zero phase) are blocked upstream; escape needs genuine intra-shell tick variance. Equidistribution is an independent Prop in this module, not supplied by the bare EightTick hypothesis.
proof idea
Definitional one-liner: cast the $\mathrm{Fin},8$ tick to a natural, then to a real, and scale by $2\pi/8$. No lemmas, tactics, or hypotheses beyond the type of the tick assignment.
why it matters
This is the phase carrier for the Gap-2 tick-phase substrate. Downstream antipodal-balance bridges apply it directly: eventual antipodal fiber-mass balance implies an oscillatory tail on this phase; antipodal balance at a fixed shell forces the exact shell amplitude of this phase to vanish by four opposite-root cancellations; tail antipodal shift composes into the same oscillatory-tail conclusion.
Certified Gap-2 Fin-8 phase close packages a named tick recipe together with decoy escapes and an oscillatory tail on this derived phase. Enriched carrier phase also builds on it. Framework landmark: T7 eight-tick octave; the unit 8th-root character is the natural Fourier mode on that cycle.
It does not flip the continuum-and-measure gate. Analytic oscillatory tail for the signature-vertex witness and strengthened late-block tail cancellation remain open (R4 / typed residual).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.