properStat
plain-language theorem explainer
Packages the proper-edge count (edges with distinct endpoints) as an additive incidence statistic on bounded complexes. Gap-2 reach-bound arguments cite it to build the proper-edge escape weight that meets gluing and atom normalizations while breaking size-blindness. The body is a structure instance wiring three already-proved proper-edge lemmas.
Claim. The proper-edge count (number of edges whose endpoints differ) is an additive incidence statistic: for every bound $B$, it assigns to each bounded complex $K$ a natural number that is invariant under relabeling, additive under disjoint union, and zero on the empty complex.
background
Gap 2 asks how far the gluing derivation of the class measure reaches without size-blindness. The derivation assumes (i) size-blindness (labeled weight depends only on the three index sizes) and (ii) gluing multiplicativity, plus unit normalizations at the three atoms (single vertex, single loop, single degenerate tetrahedron).
An additive incidence statistic is a $\mathbb{N}$-valued function of a complex that is relabeling-invariant, adds over disjoint unions, and vanishes on the empty complex. The three index sizes qualify; so do the loop count and the proper-edge count (edges with distinct endpoints). For any such statistic and $\lambda>0$, the weight $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ is invariant, positive, unit on the empty complex, and satisfies premise (ii) wherever automorphism counts multiply.
The three atom normalizations kill the loop-count escape (the single loop has loop count one) but leave the proper-edge escape untouched, since that statistic vanishes on every single-vertex complex.
proof idea
One-line structure instance for AdditiveStat. The statistic field is the proper-edge count (ignoring the bound argument). Invariance, additivity over disjoint union, and vanishing on the empty complex are discharged by the three sibling lemmas already proved for that count: invariance under equivalence, exact additivity on dunion, and zero on emptyComplex.
why it matters
This is the statistic the reach bound needs: it yields an escape weight that satisfies every hypothesis the gluing derivation places on the weight except premise (i), is normalized at the three atoms, and is not size-blind. Downstream, properEscape_normalizedAtTheAtoms, properEscape_not_sizeBlind, and properEscape_classMass_ne_mu show the escape meets the normalizations, fails size-blindness, and has class mass different from the RS measure $\mu$.
fine_horn_survives_the_other_hypotheses uses it as the concrete fine invariant separating same-size pairs (two-bridges vs two-loops) while a weight blind to it still satisfies the other five hypotheses. In the posting layer, postedWeight_incidenceCost identifies the incidence-cost posted weight with statWeight properStat at tilt $e^{-t}$, so the escape is realizable inside the formalism as a well-formed letter cost. That is the negative half of Gap 2: the other five hypotheses do not force size-blindness, and the posting layer cannot close the gap by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.