selfLoopCount_congr
plain-language theorem explainer
Self-loop count on an exact combinatorial complex is invariant under exact relabelings of the same signature. Gap2 enriched-carrier work cites this to move the self-loop invariant across isomorphic complexes before lifting to global equivalence. The proof is a Finset filter-image argument: edge bijection preserves the loop predicate, then card is preserved by injectivity.
Claim. Let $K$ and $K'$ be exact complexes of common signature $(v,e,t)$ (exactly $v$ vertices, $e$ edges, $t$ tetrahedra, with incidence maps and no cap inequalities). If $r$ is an exact relabeling isomorphism $K\simeq K'$ (bijections of vertex/edge/tet indices commuting with incidence), then the number of self-loop edges of $K$ equals that of $K'$.
background
An ExactComplex is a cap-free combinatorial complex of fixed signature: maps sending each edge index to an ordered pair of vertex indices and each tetrahedron index to four vertices. There are no size caps, so the cross-cap identification issues of bounded complexes do not arise. An exact relabeling is a triple of bijections on the vertex, edge, and tet index sets that intertwine those incidence maps (in particular, the image of an edge's endpoints is the endpoints of the image edge).
Self-loop count is the cardinality of the set of edge indices whose two endpoints coincide. The ambient module banks the enriched-carrier API for the continuum R5 residual (existence of a nontrivial oscillatory tail phase), after signature-level Fin-8 attacks stalled. The self-loop count is one concrete quotient-internal invariant used to characterize carrier ticks that escape shell-signature ticks.
Upstream, the edge-endpoint map and the relabeling's edge-commutation lemma supply the commuting square needed to transport the loop predicate.
proof idea
Classical mode; unfold the count to a filtered Finset.card on Fin e. Let $\varepsilon$ be the edge bijection of the relabeling. For each edge index, the edge-commutation identity plus injectivity of the vertex bijection give an iff: the source edge is a self-loop exactly when its $\varepsilon$-image is a self-loop.
From that iff, the filtered self-loop set of $K'$ equals the image under $\varepsilon$ of the filtered self-loop set of $K$ (membership both ways via $\varepsilon$ and $\varepsilon^{-1}$). Rewrite the target card along that equality and apply Finset.card_image_of_injective with $\varepsilon$ injective.
why it matters
Immediate parent is selfLoopCount_ge_invariant, which obtains an exact relabeling from a global equivalence and applies this congruence, so self-loop count is a global equivalence invariant of exact complexes.
In the Seven Gaps gravity stack this is part of the Wave C / route-C banking for the enriched-carrier phase below ExactPathClass. The module implements decision D-qg-c1-r4-enriched-carrier against the continuum R5 residual (nontrivial oscillatory tail). Route A (eventual mass balance / identical-zero late amplitudes from the self-loop invariant alone) refused; this lemma still closes the congruence half of the carrier API so later characterization and bridge lemmas can name the sharper typed residual. R5 itself stays open; the lemma does not flip gap2_continuum_and_measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.