selfLoopClassTick_twoLoops
plain-language theorem explainer
On the two-loop exact path class at shell index 2, the descended self-loop tick evaluates to the Fin-8 residue 2. Anyone separating quotient-internal phase from shell-signature ticks cites this evaluation. The proof is a short simplification through descent, the labeled tick, and the count lemma for the two-loop complex.
Claim. Let $C_2$ be the exact path class of the two-loop complex at shell index $n=2$. The descended self-loop class tick satisfies $\tau_{\mathrm{sl}}(2,C_2)=2\in\mathbb{F}_8$ (i.e., the self-loop count modulo 8 is exactly 2).
background
This module banks an enriched-carrier API for the continuum R5 residual after signature-level Fin-8 attacks stalled. The residual asserts an oscillatory tail phase distinct from the zero phase; the design choice is a quotient-internal tick that escapes pure shell-signature dependence.
A labeled tick assigns to each exact complex a residue in $\mathbb{F}_8$. The self-loop tick takes the number of self-loops in the complex, reduced mod 8. Descent along a global equivalence invariant pushes that labeled tick to exact path classes: evaluating the descended tick on a class recovers the labeled value on any representative complex.
The two-loop class is the path class of a concrete two-vertex complex with two self-loops (double-edge signature). An upstream count lemma records that this complex has self-loop count exactly 2.
proof idea
One-step simp only through the definition stack. Unfold the class tick as the descent of the self-loop labeled tick; unfold the two-loop class as the quotient of the two-loop complex; apply the descent evaluation identity (descended tick on a class equals the labeled tick on the representative); unfold the labeled tick as count mod 8; finish with the count lemma that the two-loop complex has exactly two self-loops. The resulting Fin-8 witness is ⟨2, _⟩ by norm_num on the bound.
why it matters
Feeds the parent theorem that the self-loop class tick is not a shell-signature tick: that proof instantiates the would-be shell factor on both the two-loop and two-bridge classes and needs the concrete value 2 on the two-loop side. The parent states that the self-loop tick uses quotient-internal incidence data and does not factor through shell signature alone.
In the Seven Gaps gravity program this is a Wave-C characterization lemma for the enriched-carrier residual under decision D-qg-c1-r4. It does not close R5 or flip the continuum-and-measure gap; it only pins a concrete class-level evaluation that witnesses escape from shell-signature ticks, supporting the sharper typed residual while R5 stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.