loopCount_dunion
plain-language theorem explainer
Loop count (edges with coincident endpoints) adds under disjoint union of bounded complexes. Gap-2 size-blindness analysis cites it when packaging the loop count as an additive incidence statistic. The proof rewrites counts as sums of loop indicators, reindexes edges by the sum-type equivalence, and uses injectivity of the left/right vertex embeddings.
Claim. For bounded complexes $K$ and $L$ (on possibly different vertex bounds), the number of loop edges in the disjoint union equals the sum of the numbers in each factor: $\mathrm{loopCount}(K \sqcup L) = \mathrm{loopCount}(K) + \mathrm{loopCount}(L)$.
background
Gap 2 studies how far the gluing derivation of the class measure reaches without size-blindness. An additive incidence statistic is a 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 incidence functions: the loop count (edges whose two endpoints coincide) and the proper-edge count (endpoints differ).
A BoundedComplex packages finite vertex/edge/tetrahedron data with an edge-endpoint map edgeVerts. Disjoint union dunion places the two complexes side by side on a sum-type vertex set, with edges reindexed by Fin nE_K ⊕ Fin nE_L via finSumFinEquiv. Sibling lemmas record that left (resp. right) edges pull back under dunion_edgeVerts_inl / dunion_edgeVerts_inr, and that the vertex injections inlV / inrV are injective.
loopCount is defined (via loopCount_eq_sum) as the sum over edges of the indicator that the two endpoints are equal. Additivity of that sum is exactly the content needed to promote loop count to an AdditiveStat.
proof idea
Classical mode. Rewrite all three sides with loopCount_eq_sum, so the claim is equality of three finite sums of 0-1 loop indicators.
Reindex the disjoint-union sum by Fintype.sum_equiv finSumFinEquiv (symmetrized) to a sum over Fin K.nE ⊕ Fin L.nE, then split with Fintype.sum_sum_type.
Left summand: Finset.sum_congr plus dunion_edgeVerts_inl. Case on whether K.edgeVerts e is already a loop. If yes, both indicators are 1. If no, the disjoint-union edge is also non-loop, because equality after inlV would force equality in K by inlV_inj.
Right summand is symmetric with dunion_edgeVerts_inr and inrV_inj.
why it matters
This is the additivity half of the loop-count additive incidence statistic in §1–§2 of the Gap-2 reach module. Downstream, loopStat installs it as the additive field of an AdditiveStat (with loopCount_invariant and loopCount_emptyComplex for the other axioms).
That package feeds the positive reach construction: for any additive statistic and any lam > 0, the weight lam^(stat K)/(nV! nE! nT!) is relabeling-invariant, positive, unit on empty, and multiplies under gluing wherever automorphism counts multiply, hence at all four CarrierShuffle families. Its class mass is lam^stat / |Aut|, so it multiplies the symmetry factor without binomial corrections.
The three atom normalizations then kill the loop-count escape (loopEscape_fails_the_atoms): the single-loop atom has loop count one, forcing weight lam ≠ 1 unless lam = 1. Proper-edge escape survives those atoms. The theorem is local combinatorics inside Gravity/SevenGaps; it does not itself touch T5–T8 or the RCL, but it sharpens which size-blindness counter-models remain after the derivation's normalizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.