statWeight_emptyComplex
plain-language theorem explainer
For any additive incidence statistic and any real tilt, the associated labeled weight of the empty complex is exactly 1. Escape-weight constructions cite this as the unit-normalization half of the gluing package. The proof unfolds the Gibbs factor, applies vanishing of the statistic on the empty complex, and evaluates the empty factorials.
Claim. Let $\varphi$ be an additive incidence statistic (relabeling-invariant, additive under disjoint union, and zero on the empty complex), let $\lambda\in\mathbb{R}$, and let $B\in\mathbb{N}$. Then the labeled weight $\lambda^{\varphi(K)}/(n_V!\,n_E!\,n_T!)$ of the empty $B$-bounded complex equals $1$.
background
Gap 2 studies how far the gluing derivation of the class measure reaches without size-blindness. Premise (i) is size-blindness (labeled weight depends only on the three index sizes); premise (ii) is gluing multiplicativity at pairs where automorphism counts multiply. The three atom normalizations pin the remaining free constants.
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. Index sizes qualify; so do loop count and proper-edge count. For any such statistic $\varphi$ and tilt $\lambda>0$, the weight $\lambda^{\varphi(K)}/(n_V!,n_E!,n_T!)$ is the Gibbs weight times a pure tilt. The Gibbs weight itself is one unit of recognition shared evenly over labelings: $1/(n_V!,n_E!,n_T!)$.
Unit value on the empty complex is one of the four structural properties needed so that such a tilted weight satisfies every hypothesis of the gluing package except size-blindness itself.
proof idea
Term-mode proof in three steps. Unfold statWeight and the underlying Gibbs weight, exposing $\lambda^{\varphi(\emptyset)}/(0!,0!,0!)$. Rewrite the exponent via the structure field that forces every additive statistic to vanish on the empty complex, so the power is $\lambda^0$. Evaluate the empty complex (all three index sizes zero) by norm_num, which reduces the factorials to $1$ and yields $1$.
why it matters
This is the empty-complex unit clause in the package that shows the other five hypotheses do not force size-blindness. Downstream, properEscape_satisfiesTheOtherHypotheses packages invariance, positivity, this unit identity, atom normalization, and gluing into a single witness that the proper-edge escape weight meets every non-size-blind hypothesis of the CarrierShuffle derivation.
Together with the loop-count escape (killed by the single-loop atom) and the proper-edge escape (which survives the atoms), the module separates premise (i) from the rest of the gluing package: size-blindness is an independent assumption, not a consequence of gluing plus normalizations. That negative reach bound is the module's main report on Gap 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.