selfLoopCount_twoLoops
plain-language theorem explainer
The two-loop exact complex (two self-loops at one vertex, signature (2,2,0)) has self-loop count exactly 2. Gap-2 gravity workers cite this when separating loop-rich carriers from bridge-only complexes under global equivalence. The proof unfolds the count and the complex, shows every Fin-2 edge is a loop, and reads off the filtered cardinality.
Claim. Let $K$ be the exact complex with $v=2$, $e=2$, $t=0$ whose every edge is the self-loop $(0,0)$. Then the number of loop edges of $K$ (edges with equal endpoints) equals $2$.
background
This module banks the enriched-carrier API for the continuum R5 residual on oscillatory tails after the Fin-8 signature attack stalled. The local setting is route C: sharper typed residuals and bridge lemmas around quotient-internal ticks that escape shell-signature ticks; R5 itself stays open.
An exact complex packages edge and tetrahedron vertex data. The self-loop count of a complex is the cardinality of the set of edge indices whose two endpoints coincide. The two-loop complex is the concrete complex of signature $(2,2,0)$ with every edge map constantly $(0,0)$ (two loops at vertex 0).
Self-loop count is designed as a global-equivalence invariant (sibling lemmas establish congruence and $\ge$-invariance), so evaluating it on named test complexes is the first step toward inequivalence certificates.
proof idea
Classical mode. Unfold the self-loop count definition and the two-loop complex. The edge map is constantly $(0,0)$, so the filter predicate "endpoints equal" holds for every $i:\mathrm{Fin},2$. Prove by ext and simp that the filtered Finset equals Finset.univ on Fin 2. Rewrite and simp to obtain cardinality $2$.
why it matters
Feeds the inequivalence ¬ GlobalEquivalent between the two-loop and two-bridge complexes: invariance of self-loop count plus this evaluation and the companion count $0$ on bridges yields $2=0$, a contradiction. Also discharges the self-loop class tick on the two-loop class, wiring the concrete count into the descended tick API.
Inside the Seven Gaps gravity stack this is scaffolding for the enriched-carrier phase attack on the continuum oscillatory-tail residual (Wave C R5), not a flip of gap2_continuum_and_measure. It supports characterization of loop-rich carriers below ExactPathClass without claiming mass balance or identical-zero late amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.