selfLoopCount
plain-language theorem explainer
Counts self-loop edges in an exact-size combinatorial complex: edges whose two endpoints coincide. Gravity/SevenGaps work uses it as a discrete invariant of the carrier graph under exact relabelings. The body is a classical Finset filter-and-card over the edge index set.
Claim. For an exact complex $K$ with $v$ vertices, $e$ edges and $t$ tetrahedra, $\mathrm{selfLoopCount}(K)$ is the number of edge indices $i\in\{0,\ldots,e-1\}$ such that both endpoints of edge $i$ are the same vertex.
background
An ExactComplex is a cap-free combinatorial complex of fixed signature $(v,e,t)$: incidence is given by maps from edge and tetrahedron indices into vertex indices, with no bounding inequalities. In particular each edge $i$ is a pair of vertices via the incidence map edgeVerts.
A self-loop is an edge whose two endpoints are equal. This definition simply counts those edges. The surrounding module banks an enriched-carrier API for the continuum R5 residual (oscillatory tail of a nontrivial phase versus the zero phase), after signature-level Fin-8 attacks stalled. The self-loop count is the raw integer from which a mod-8 labeled tick is later built.
Upstream geometry modules supply analogous edgeVerts maps on Freudenthal triangulations; here the same name is the incidence field of the exact complex, not a fixed cube edge list.
proof idea
Definition by classical choice: filter the finite set of all edge indices Fin e to those $i$ with equal endpoints under K.edgeVerts, then take cardinality. No lemmas are applied; it is a one-shot Finset expression.
why it matters
This count is the carrier-side integer invariant feeding the enriched-carrier phase attack on Gap 2. Downstream, congruence under exact relabeling and under global equivalence are proved immediately, so the count descends to equivalence classes of complexes. Concrete evaluations pin twoLoopsComplex at 2 and twoBridgesComplex at 0, separating loop-rich from bridge-only carriers.
The main consumer is the labeled tick that reduces the count modulo 8, together with its global-equivalence invariance. That tick is the quotient-internal discrete phase the module uses to escape shell-signature ticks while keeping R5 open: eventual fiber-mass balance from the self-loop invariant alone was refused, so the residual is sharpened rather than closed. No claim is made on gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.