selfLoopTick_invariant
plain-language theorem explainer
The self-loop count modulo eight is constant on global-equivalence orbits of exact complexes, so it is a well-typed labeled tick. Anyone packaging quotient-level phase data for the Gap-2 continuum residual cites this invariance. The proof reduces Fin-8 equality to the already-proved invariance of the raw self-loop count under global equivalence.
Claim. The labeled tick that sends each exact complex to its self-loop count modulo $8$ is a global-equivalence invariant: for all dimensions $v,e,t$ and exact complexes $K,K'$ of that type, if $K$ and $K'$ are globally equivalent then their self-loop ticks agree as elements of $\mathrm{Fin}\,8$.
background
This module implements the Wave-C R5 attack on the continuum residual that asserts an oscillatory tail for some phase but not for the zero phase. Signature-level Fin-8 blockers stalled (mesoscopic cube dominance only), so route C banks an enriched-carrier API: labeled ticks that descend to exact path classes once they are constant on global-equivalence orbits.
A labeled tick assigns each exact complex a value in $\mathrm{Fin},8$, the eight-tick octave. The enrichment hypothesis GlobalEquivalentInvariant says the assignment is constant whenever two complexes are globally equivalent. The self-loop tick is the self-loop count of the complex, reduced modulo 8. The RS tick quantum and the period-8 octave fix that codomain.
Upstream, the raw count is already known to be invariant under global equivalence (selfLoopCount_ge_invariant); this theorem only lifts that fact to the Fin-8 labeled tick.
proof idea
Introduce the two exact complexes and the global-equivalence hypothesis. The goal is equality in $\mathrm{Fin},8$. Apply Fin.ext to reduce to equality of the underlying naturals, then change the goal to equality of self-loop counts modulo 8. A single rewrite by selfLoopCount_ge_invariant (the count itself is invariant under the given equivalence) closes the proof. Short tactic script, no new arithmetic.
why it matters
This is the invariance certificate required to descend the self-loop tick to exact path classes via descendedTick, yielding the class-level tick selfLoopClassTick. That tick is then packaged into selfLoopEnrichedSubstrate, the concrete enriched-carrier phase substrate aimed at the Gap-2 continuum oscillatory-tail residual.
In the Recognition framework the codomain $\mathrm{Fin},8$ is the eight-tick octave forced at T7. The construction escapes ShellSigTick and supplies a quotient-internal phase carrier below ExactPathClass. R5 itself stays open: eventual fiber-mass balance (or identical-zero late amplitudes) from the self-loop invariant alone was refused in-session, so the residual remains uninhabited. The module does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.