loopCount_eq_sum
plain-language theorem explainer
The loop count of a bounded complex equals the sum of indicator values that mark edges whose two endpoints coincide. Anyone proving additivity or relabeling invariance of loop count cites this identity. The proof is a two-step term rewrite: unfold the definition and apply the standard card-of-filter-to-sum lemma.
Claim. For every bounded complex $K$, the loop count of $K$ equals $\sum_{i < n_E(K)} \mathbf{1}_{\{u_i = v_i\}}$, where $(u_i,v_i)$ are the endpoints of the $i$-th edge of $K$.
background
This module sits inside Gap 2 of the gravity seven-gaps program. Gap 2 asks how far the gluing derivation of the class measure reaches once size-blindness is treated as a hypothesis rather than a theorem. An additive incidence statistic is any natural-valued function of a complex that is relabeling-invariant, additive over disjoint unions, and zero on the empty complex. The three index sizes qualify; so do two pure incidence counts: the loop count (edges with equal endpoints) and the proper-edge count (edges with distinct endpoints).
loopCount is defined as the cardinality of the set of edge indices whose two endpoints agree. The present identity rewrites that cardinality as an explicit sum of 0-1 indicators over Fin nE. That sum form is the natural one for proving additivity under disjoint union, because the edge set of a disjoint union is the tagged sum of the two edge sets and the indicators split accordingly.
The surrounding development uses this statistic to build weights of the form $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$, which satisfy gluing multiplicativity wherever automorphism counts multiply, yet leave the symmetry factor $|\mathrm{Aut}|$ untouched.
proof idea
Two-line term proof. Unfold the definition of loop count (cardinality of the filtered edge-index set). Rewrite with Finset.card_filter, which converts the cardinality of a decidable filter into the sum of the corresponding 0-1 indicators over the whole finite type Fin nE. No case splits and no complex-specific lemmas are required.
why it matters
This identity is the computational hinge for loopCount_dunion, the theorem that loop count is additive over disjoint unions. Additivity is one of the three axioms of an additive incidence statistic in §1–§2 of the Gap 2 reach analysis. With additivity in hand, the module constructs the loop-count escape weight $\lambda^{\mathrm{loopCount}(K)}/|\mathrm{Aut},K|$ and shows it satisfies premise (ii) (gluing multiplicativity) at every pair the CarrierShuffle derivation uses.
The three atom normalizations then kill that escape: the single-loop atom has loop count one, so its weight is $\lambda$ rather than 1 (loopEscape_fails_the_atoms). The identity therefore feeds the positive half of the reach bound: the other five hypotheses do not force size-blindness, because loop-count (and proper-edge) weights still glue, yet the normalizations pin which statistic can survive. It does not itself close Gap 2; it equips the additive-statistic toolkit that makes the reach and non-implication statements precise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.