loopCount_emptyComplex
plain-language theorem explainer
The loop count of the empty complex is zero for every natural parameter B. Anyone packaging loop count as an additive incidence statistic cites this vanishing clause. The proof is a one-line simplification that unfolds the two definitions.
Claim. For every natural number $B$, the number of edges whose two endpoints coincide on the empty complex (parameterized by $B$) equals $0$.
background
Gap 2 asks how far the gluing derivation's size-blindness premise reaches. An additive incidence statistic is a natural-valued function of a complex that is relabeling-invariant, additive over disjoint unions, and vanishes on the empty complex. The three index sizes qualify; so do two pure incidence counts: loop count (edges with coincident endpoints) and proper-edge count (edges with distinct endpoints).
Loop count is built only from incidence data, not from the three sizes. The empty complex is the zero object for disjoint union, so every additive statistic must send it to zero. That vanishing axiom is exactly what this lemma records for loop count.
The surrounding module shows that weights of the form $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ satisfy gluing multiplicativity wherever automorphism counts multiply, and therefore supply escapes from size-blindness unless further normalizations kill them.
proof idea
One-line tactic proof: simp unfolds loopCount and emptyComplex. Both definitions make the empty complex contribute no edges, so the filtered count of self-incident edges is definitionally zero.
why it matters
This lemma is the vanishes field of loopStat, the AdditiveStat package for loop count. That package is the positive half of the reach bound in Gap 2: loop count is a genuine additive incidence statistic, so the associated fugacity weight $\lambda^{\mathrm{loopCount}(K)}/|\mathrm{Aut},K|$ satisfies premise (ii) and is not forced by the other five hypotheses to be size-blind.
The three unit normalizations later kill this particular escape (loopEscape_fails_the_atoms), because the single-loop atom has loop count one. Proper-edge count survives those normalizations. The lemma therefore sits at the hinge between "the escape exists" and "the normalizations are not idle." It does not itself touch the Recognition forcing chain (T0–T8) or the RCL; it is local to the gravity Gap-2 audit of the class-measure derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.