selfLoopCount_ge_invariant
plain-language theorem explainer
Global equivalence of exact complexes preserves self-loop count. Continuum-residual and Gap-2 workers cite it to make enriched-carrier phase labels (and Fin-8 ticks built from the count) well-defined on the quotient. Proof unpacks the equivalence witness and applies the existing count-congruence lemma.
Claim. Let $K$ and $K'$ be exact complexes with the same type parameters. If $K$ and $K'$ are globally equivalent, then the self-loop count of $K$ equals the self-loop count of $K'$.
background
This module banks the enriched-carrier API for the Wave-C R5 attack on Gap 2's continuum residual (oscillatory tail below the exact path class). After the Fin-8 signature blocker stalled, the session records carrier descent and a quotient-internal tick that escapes the shell-signature tick, while leaving R5 itself open and uninhabited.
An exact complex packages the combinatorial shell/gauge data at fixed vertex, edge, and tick parameters. Global equivalence identifies complexes related by the allowed global rewrites. Self-loop count is the number of edges with identical source and target; a sibling congruence already shows the count is stable under the underlying rewrite witness.
The eight-tick octave (period $2^3$ from the forcing chain) makes counts modulo 8 the natural phase labels on the quotient. Invariance of the raw count is the bridge to those labels.
proof idea
Short term proof. Global equivalence is a structure whose sole field is a rewrite witness. Destructure the hypothesis to obtain that witness, then apply the sibling congruence lemma that already equates self-loop counts along a rewrite. No arithmetic, induction, or case split.
why it matters
Two same-module parents consume it. The self-loop-tick invariant rewrites the equality as equality of counts mod 8 and registers the self-loop tick as a global-equivalence invariant (the enriched-carrier phase label on the quotient). The two-loops-versus-two-bridges non-equivalence applies it and reduces to $2 \neq 0$, separating those complexes in the characterization layer.
That separation supports the sharper typed residual naming the enriched-carrier obligation after route A (eventual mass balance) refused and route B (Fin-8 signature blocker) was dropped. Framework landmark in play is the eight-tick octave. R5 and gap2_continuum_and_measure stay open; this lemma only stabilizes the carrier count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.