loopStat
plain-language theorem explainer
Packages the loop count (edges with coincident endpoints) as an additive incidence statistic on bounded complexes. Gravity Gap-2 arguments cite it to build the loop-count escape weight that satisfies gluing multiplicativity without size-blindness. The body is a four-field structure instance discharging invariance, disjoint-union additivity, and vanishing on the empty complex from prior loopCount lemmas.
Claim. The loop count of a bounded complex (number of edges whose two endpoints coincide) is an additive incidence statistic: it is invariant under relabeling equivalence, additive under disjoint union of complexes, and equals zero on every empty complex. The bound parameter is ignored, so the statistic is a single function of the complex rather than a cap-indexed family.
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 bounded complex that is relabeling-invariant, adds over disjoint unions, and vanishes on the empty complex. The three index sizes qualify; so do two incidence reads: loop count (coincident endpoints) and proper-edge count (distinct endpoints).
The module shows that for any such statistic and any positive real $\lambda$, the weight $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ is relabeling-invariant, positive, unit on the empty complex, and multiplies under disjoint union wherever automorphism counts multiply. Its class mass is $\lambda^{\mathrm{stat}}/|\mathrm{Aut}|$, leaving the symmetry factor intact.
Upstream, loopCount counts loops in an edge sequence (cardinality of the loop set). The three field lemmas used here already establish that this count is invariant under equivalence, additive on disjoint union, and zero on the empty complex.
proof idea
Four-field structure instance for AdditiveStat. The statistic field is fun _ K => loopCount K (cap ignored). Invariance is loopCount_invariant; additivity is loopCount_dunion; vanishing is loopCount_emptyComplex. No new arithmetic: pure packaging of the three prior loop-count lemmas into the additive-statistic interface.
why it matters
This is the loop-count escape used to attack premise (i) of the Gap-2 gluing derivation. Downstream, loopEscape_not_sizeBlind shows the associated weight fails size-blindness for $\lambda\neq 1$; loopEscape_fails_the_atoms shows the three atom normalizations kill it because the single loop has loop count one, so the weight there is $\lambda$. The control case loopEscape_sizeBlind_at_one recovers size-blindness at $\lambda=1$.
classMass_gibbsWeight_eq_mu identifies the unit-tilt Gibbs class mass with the RS measure by equating the Gibbs weight to statWeight loopStat 1. The sibling properStat is the surviving escape: proper-edge count vanishes on the atoms, so normalizations do not kill it, and the reach bound is carried there. Within RS gravity this separates what gluing multiplicativity alone can force from what size-blindness must still assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.