properEdgeCount_emptyComplex
plain-language theorem explainer
The proper-edge count of the empty complex is zero for every bond parameter. Anyone packaging proper-edge count as an additive incidence statistic cites this vanishing clause. The proof is a one-line appeal to the lemma that proper-edge count vanishes whenever the complex has at most one vertex, discharged by simplifying the empty complex.
Claim. For every natural number $B$, the number of edges with distinct endpoints in the empty complex on parameter $B$ equals $0$.
background
Gap 2 asks how far the gluing premise of the class-measure derivation reaches, and whether size-blindness (premise (i): labeled weight depends only on the three index sizes) is forced by the other hypotheses. An additive incidence statistic is a natural-valued function of a complex that is relabeling-invariant, additive under disjoint union, and zero on the empty complex. The three index sizes qualify; so do two incidence reads: loop count (edges with coincident endpoints) and proper-edge count (edges with distinct endpoints).
Proper-edge count is the statistic that survives the three atom normalizations and supplies the escape weight $\lambda^{\mathrm{proper}}/|\mathrm{Aut}|$, which multiplies the symmetry factor without binomial correction. The empty-complex vanishing axiom is one of the three defining properties of an additive incidence statistic; without it the packaging into that structure type fails.
proof idea
One-line term proof. Apply the general lemma that proper-edge count is zero on any complex with at most one vertex, then discharge the size hypothesis by simp on the definition of the empty complex (which has zero vertices, hence $n_V \le 1$).
why it matters
This is the vanishes field of properStat, the additive-incidence-statistic package for proper-edge count. That package is the positive half of the reach bound in §1–§3: weights of the form $\lambda^{\mathrm{stat}}/(n_V!,n_E!,n_T!)$ glue multiplicatively wherever automorphism counts multiply, leave the symmetry factor untouched, and (for proper-edge count) pass the three atom normalizations that kill the loop-count escape. Downstream, the proper-edge escape shows that the other five hypotheses do not force size-blindness; only the normalizations select among additive statistics, and they leave proper-edge free. The result is local bookkeeping inside Gap 2, not a forcing-chain landmark (T0–T8), but it pins why premise (i) remains an independent assumption in the class-measure derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.