selfLoopClassTick
plain-language theorem explainer
The self-loop count modulo 8, pushed down from labeled exact complexes to exact path classes of complexity n. Gravity and continuum-residual workers cite it as the concrete quotient-internal Fin-8 tick that escapes shell-signature-only phases. It is a one-line application of the invariant labeled-tick descent combinator to the self-loop count map.
Claim. For every complexity $n\in\mathbb{N}$, there is a map from the exact path class of complexity $n$ (shell signature plus global-equivalence quotient of exact labeled complexes) to $\mathrm{Fin}\,8$, obtained by descending the labeled tick that sends each complex to its self-loop count modulo $8$.
background
The ambient module banks an enriched-carrier API for the continuum R5 residual (existence of a nontrivial oscillatory tail phase). Signature-level Fin-8 attacks stalled; the design choice is a quotient-internal tick that can see incidence data below shell signature.
An exact path class of complexity $n$ is a shell signature paired with a global-equivalence class of exact labeled complexes of that signature (no bounded-complex cap). A labeled tick assigns a value in $\mathrm{Fin},8$ to each exact labeled complex. Global-equivalence invariance means the assignment is constant on equivalence classes, so it descends via quotient lift.
The self-loop labeled tick is self-loop count mod 8; invariance follows because global equivalence preserves self-loop count. Descent of an invariant labeled tick is the standard Quotient.lift along the exact setoid.
proof idea
One-line wrapper: apply the general descent combinator for invariant labeled ticks to the self-loop labeled tick and its global-equivalence invariance theorem. No extra case analysis; the body is exactly that application.
why it matters
This is the concrete class-level tick used to build the self-loop derived phase (tick-to-real phase map on exact path classes). Downstream it feeds the witness that the tick does not factor through shell signature alone: on complexity 2 it evaluates to 2 on the two-loops class and to 0 on the two-bridges class, which share a signature, so the tick is not a shell-signature tick.
In the Seven Gaps / Gap2 continuum story this is the enriched-carrier object that escapes the mesoscopic-only cube-dominance blockage. It does not close R5 or flip the continuum-and-measure gap; it only supplies the sharper carrier and the non-factorization lemmas that route C needs while the residual stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.