loopEscape_fails_the_atoms
plain-language theorem explainer
The three unit normalizations force any admissible labeled weight to equal 1 on the single-loop atom. The loop-count escape weight with fugacity λ ≠ 1 evaluates to λ there, so it fails those normalizations. Gap-2 reach-bound arguments cite this to discard the loop-count escape and force the surviving statistic to vanish on the atoms. The proof is a direct evaluation at the one-loop bouquet.
Claim. For every real $\lambda \neq 1$, the labeled weight $w(K)=\lambda^{\mathrm{loop}(K)}/(n_V!\,n_E!\,n_T!)$ fails the three unit normalizations: it is not equal to $1$ on every one-vertex complex with at most one incidence (the atoms).
background
Gap 2 asks how far the gluing derivation of the class measure reaches. That derivation takes two premises (size-blindness of the labeled weight, and gluing multiplicativity where automorphism counts multiply) plus three unit normalizations: the weight equals 1 at the three atoms (single vertex, single loop, single degenerate tetrahedron).
An additive incidence statistic is relabeling-invariant, additive on disjoint unions, and zero on the empty complex. Loop count (edges with coincident endpoints) is one such statistic. For any positive real $\lambda$, the associated escape weight $\lambda^{\mathrm{stat}(K)}/(n_V!,n_E!,n_T!)$ satisfies gluing multiplicativity and leaves the symmetry factor $|\mathrm{Aut}|^{-1}$ intact, multiplying it by $\lambda^{\mathrm{stat}}$.
NormalizedAtTheAtoms restates the three unit conditions off the size function: the weight is 1 at every complex with one vertex and at most one incidence. The module shows those normalizations discriminate among escape statistics.
proof idea
Assume for contradiction that the loop-count escape weight at $\lambda$ is normalized at the atoms. Instantiate that hypothesis on the one-loop bouquet (one vertex, one loop edge). Loop count of that bouquet is 1 by decision procedure, and its bare Gibbs factorial weight is 1. Unfolding the escape weight therefore collapses it to $\lambda^1\cdot 1=\lambda$. Normalization demands the value 1, so $\lambda=1$, contradicting the hypothesis $\lambda\neq 1$.
why it matters
This is the sharp negative half of §3 in the Gap-2 reach module: the three normalizations have real force and kill the loop-count escape. Downstream, ReachIndex records exactly that fact as a compiled control bit, and the module introduces properStat (proper-edge count) because it vanishes on every single-vertex complex, atoms included, and therefore survives the same normalizations.
Parent results that depend on the discrimination include properEscape_classMass_ne_mu (the proper-edge escape has class mass $\lambda^2/|\mathrm{Aut}|$ on the two-bridge class, not the RS measure $1/|\mathrm{Aut}|$) and the blindness lemmas that package the reach bound. Without this theorem the reach bound could be read as an artifact of a malformed escape rather than a genuine gap in the five remaining hypotheses. It does not itself touch T5–T8 or the RCL; it is local gravity/measure scaffolding for why size-blindness must be assumed rather than derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.