loopCount
plain-language theorem explainer
Counts how many edges of a bounded complex have both endpoints equal (true loops). Gravity and census authors cite it as the incidence statistic that is additive and relabeling-invariant yet independent of the three index sizes. The definition is a one-line Finset filter-and-card on the edge-vertex map.
Claim. For a bounded complex $K$, $\mathrm{loopCount}(K)$ is the number of edges $e$ with both endpoints equal: $\#\{ i < n_E(K) : v_0(e_i)=v_1(e_i)\}$.
background
Gap 2 asks how far the gluing derivation of the class measure reaches without size-blindness. Size-blindness says the labeled weight depends only on the three index sizes $(n_V,n_E,n_T)$. The module studies additive incidence statistics: natural-valued functions of a complex that are relabeling-invariant, additive over disjoint unions, and zero on the empty complex.
The three index sizes are such statistics. So are two pure incidence counts: the loop count (edges with coincident endpoints) and the proper-edge count (edges with distinct endpoints). A bounded complex $K$ carries edge incidence data edgeVerts, sending each edge index to an ordered pair of vertices. Loop count is the cardinality of the set of edge indices whose pair is diagonal.
The module doc stresses that this is a function of incidence data that is not a function of the three index sizes, so it can seed weights of the form $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ that still glue where automorphism counts multiply.
proof idea
Definition, not a proof. Unfold to the cardinality of the Finset of all edge indices $i:\mathrm{Fin},n_E(K)$ such that the two components of edgeVerts i are equal. No lemmas are applied at the definition site; later theorems (loopCount_eq_sum, loopCount_congr, loopCount_dunion, loopCount_emptyComplex) rephrase and establish the additive-incidence axioms from this filter.
why it matters
This is the first of the two non-size incidence statistics in §1 of the Gap 2 reach analysis. Downstream, loopCount_congr shows it is a class function, loopCount_dunion and loopCount_emptyComplex show additivity and vanishing on the empty complex, and loopCount_eq_sum gives the sum form used in those proofs.
In the census product form it reappears as the loop tally on edge sequences, cutting cells $\mathrm{Cell}(n,k,j)={f:\mathrm{loopCount}(f)=j}$, and is invariant under the census group action (loopCount_smul). The ensemble-nonempty instance builds the empty sequence as a zero-loop cell via this count.
Framework role: it supplies the loop-count escape weight $\lambda^{\mathrm{loopCount}}/|\mathrm{Aut}|$. The three atom normalizations kill that escape (loopEscape_fails_the_atoms) because the single-loop atom has loop count one, while they leave the proper-edge escape alive. Thus the definition is the positive half of the reach bound: other hypotheses do not force size-blindness; only the atom normalizations pin which statistic survives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.