selfLoopTick
plain-language theorem explainer
Defines a Fin-8 labeled tick that returns the self-loop edge count of an exact complex, reduced modulo 8. Gap2 enriched-carrier work cites it as the concrete quotient-internal phase that escapes ShellSigTick. Construction is direct: cardinality of equal-endpoint edges, then mod 8 with the Fin bound by norm_num.
Claim. Define a labeled tick $\tau$ on exact complexes by $\tau(K) := \#\{i : \text{both endpoints of edge }i\text{ equal}\} \bmod 8 \in \mathrm{Fin}\,8$. The value depends only on the complex $K$, not on the ambient vertex/edge/triangle counts.
background
This module banks the Wave C R5 attack surface after the signature-level Fin-8 oscillatory-tail blocker stalled. The continuum residual asks for a phase with an oscillatory tail that the zero phase lacks. Route A (eventual mass balance on an enriched carrier) is design-correct but refused in-session; route C is the terminal credit path: name a sharper typed residual and supply carrier API plus a concrete tick outside ShellSigTick.
A labeled tick is a map from exact complexes (for any vertex/edge/triangle counts) into $\mathrm{Fin},8$. The self-loop count is the number of edges whose two endpoints coincide. Reducing that count mod 8 lands in the eight-tick octave forced by the T7 landmark (period $2^3$). The dimensionless bridge ratio $K=\varphi^{1/2}$ appears only as ambient constant infrastructure, not in the tick formula itself.
proof idea
Definition, not a proof. Ignore the three size parameters; on complex $K$ evaluate self-loop count, reduce modulo 8, and pack the residue as an element of $\mathrm{Fin},8$ via $\mathrm{Nat.mod_lt}$ with the trivial bound $0<8$. No lemmas beyond that arithmetic fact.
why it matters
Anchor of the enriched-carrier API for Gap2. Downstream, selfLoopTick_invariant shows constancy on GlobalEquivalent orbits; selfLoopClassTick descends it to exact path classes; the twoLoops/twoBridges evaluations witness distinct class values $\langle 2\rangle$ and $\langle 0\rangle$; selfLoopEnrichedSubstrate packages the tick plus invariance plus the not-ShellSigTick witness as an EnrichedCarrierPhaseSubstrate.
That substrate is the concrete object route C needs for the typed residual TypedResidual_continuum_substrate_oscillatoryTail. It does not close R5 (still OPEN/uninhabited) and does not flip gap2_continuum_and_measure. Framework contact is the eight-tick octave (T7): the mod-8 reduction is exactly the period-$2^3$ clock on loop incidence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.