selfLoopPhase
plain-language theorem explainer
Self-loop phase assigns each exact path class of complexity n a real angle built from its self-loop Fin-8 tick. Continuum-residual and Gap-2 workers cite it when wiring an enriched-carrier oscillatory phase under ExactPathClass. The body is a one-line composition of the standard tick-to-phase map with the descended self-loop class tick.
Claim. For every $n\in\mathbb{N}$ and every exact path class $c$ of complexity $n$, the self-loop phase is the real $$2\pi\cdot\tau(c)/8,$$ where $\tau(c)\in\{0,\ldots,7\}$ is the Fin-8 tick obtained by descending the self-loop count of any labeled representative of $c$ through the global-equivalence quotient.
background
Exact path classes are the exact complexity shell: for fixed $n$, the disjoint union over shell signatures of the quotient of exact labeled complexes by global equivalence. No bounded-complexity cap appears in that type.
The module banks an enriched-carrier API for the Wave C R5 attack on the continuum residual that asserts existence of a nontrivial oscillatory tail phase. After the Fin-8 signature blocker stalled, the session chose route C: name a sharper typed residual and characterize a concrete quotient-internal tick that escapes the shell-signature tick predicate.
Upstream, the tick-derived phase map sends any Fin-8-valued class function $\tau$ to the angle $2\pi\cdot(\tau,n,c)/8$. The self-loop class tick is that map applied after descending the self-loop count through the global-equivalence invariant, so the phase is well-defined on the quotient. The fundamental RS tick is the unit time quantum $\tau_0=1$; the eight-tick octave is the evolution period $2^3$.
proof idea
One-line definitional wrapper. Instantiate the generic tick-derived phase constructor at the already-built self-loop class tick (itself descendedTick of the self-loop tick through its global-equivalence invariance). No tactics, no new arithmetic: the phase is definitionally $2\pi$ times the natural value of that Fin-8 tick, divided by 8.
why it matters
This is the phase leg of the enriched-carrier stack under ExactPathClass for Gap 2. It turns the self-loop class tick into the real-valued oscillatory phase that the continuum R5 residual talks about (existence of a phase with oscillatory tail not shared by the zero phase).
It sits on the T7 eight-tick octave: phases are eighth-roots of unity angles. The module doc is explicit that route A (eventual mass balance / identical-zero late amplitudes for this tick) refused in-session, route B (signature Fin-8 oscillatory-tail blocker) was already dead, and the credit-bearing terminal is route C: sharper residual plus carrier API. R5 itself stays open; this definition does not flip gap2_continuum_and_measure and introduces no sorry or axiom.
No downstream consumers are wired yet; the declaration exists so later bridge lemmas can quote a concrete phase on the self-loop carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.