AdditiveStat
plain-language theorem explainer
An additive incidence statistic is a natural-valued functional on bounded complexes that is relabeling-invariant, additive under disjoint union, and zero on the empty complex. It packages the exact algebraic properties shared by the three index sizes, the loop count, and the proper-edge count. Anyone studying Gap 2 escapes from size-blindness cites it: weights built as λ^stat over factorial denominators glue multiplicatively wherever automorphism counts multiply, so the restricted gluing premise cannot force size-blindness alone.
Claim. An additive incidence statistic is a structure consisting of a map $\mathrm{stat}_B$ sending each bounded complex of cap $B$ to a natural number, such that (i) if $K\simeq K'$ by relabeling then $\mathrm{stat}_B(K)=\mathrm{stat}_B(K')$, (ii) $\mathrm{stat}_{B+B'}(K\sqcup L)=\mathrm{stat}_B(K)+\mathrm{stat}_{B'}(L)$, and (iii) $\mathrm{stat}_B(\emptyset_B)=0$.
background
Gap 2 asks how far the gluing premise of the class-measure derivation reaches, and why the posting layer cannot close size-blindness. The derivation in Gap2GluingDerivation obtains the class measure from two premises plus three atom normalizations: (i) size-blindness (labeled weight depends only on the three index sizes $n_V,n_E,n_T$), and (ii) gluing multiplicativity of class mass over disjoint unions at pairs where automorphism counts multiply.
An additive incidence statistic isolates the algebraic skeleton shared by the three index sizes and by two pure incidence counts: the loop count (edges with coincident endpoints) and the proper-edge count (edges with distinct endpoints). Bounded complexes carry finite vertex/edge/tetrahedron data under a cap $B$; equivalence is relabeling; disjoint union dunion concatenates two complexes at summed caps; the empty complex is the zero object at each cap.
The module shows that any such statistic, paired with a positive real $\lambda$, yields a weight $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ that is relabeling-invariant, strictly positive, unit on the empty complex, and satisfies premise (ii) at every pair whose automorphism counts multiply. No binomial correction appears because the statistic adds exactly where $|\mathrm{Aut}|$ multiplies.
proof idea
No proof body: this is a structure declaration packing four fields. Downstream instances discharge the fields by existing lemmas. For the loop-count instance, stat ignores the cap and returns loopCount; invariance is loopCount_invariant; additivity is loopCount_dunion; vanishing is loopCount_emptyComplex. The proper-edge instance is analogous via properEdgeCount_*. The three index sizes are the motivating examples already known to be additive and invariant.
why it matters
This structure is the exact level of generality at which restricted gluing fails to force premise (i). It feeds statWeight, whose class mass is $\lambda^{\mathrm{stat}(K)}/|\mathrm{Aut},K|$ (classMass_statWeight), leaving the RS symmetry factor untouched and tilting it by $\lambda^{\mathrm{stat}}$. At $\lambda=1$ the same formula recovers the RS measure exactly (classMass_statWeight_at_one), so later inequalities measure pure tilt.
Concrete escapes are the instances loopStat and properStat. The three atom normalizations kill the loop-count escape (the single loop has loop count one, so its weight is $\lambda\neq 1$), but leave the proper-edge escape alive, since proper-edge count vanishes on every single-vertex complex. The refined invariant sizeStatInvariant adjoins the statistic to the three cell counts and separates those witnesses.
In the Seven Gaps gravity program this pins Gap 2's negative reach bound: gluing multiplicativity plus the four CarrierShuffle families see only additivity, not whether the statistic reads pure size. Size-blindness remains an independent premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.