NormalizedAtTheAtoms
plain-language theorem explainer
A labeled weight on bounded complexes is normalized at the atoms when it equals 1 on every complex with one vertex and at most one incidence. Those three complexes are the single vertex, the single loop, and the single degenerate tetrahedron. Anyone citing the Gap-2 fugacity or posting-gluing results uses this as the common atom-normalization premise. The body is a pure Prop abbreviation, not a proved statement.
Claim. A labeled weight $w$ (assigning a real to every bounded complex of every bound $B$) is normalized at the atoms when $w_B(K)=1$ whenever $K$ has exactly one vertex and $n_E(K)+n_T(K)\le 1$. Equivalently, $w=1$ on the three atoms $(n_V,n_E,n_T)\in\{(1,0,0),(1,1,0),(1,0,1)\}$.
background
Gap 2 studies how far the gluing premise of the class-measure derivation reaches, and why the posting layer cannot close the remaining freedom. The derivation starts from size-blindness (the labeled weight depends only on the three index sizes $n_V,n_E,n_T$) and gluing multiplicativity (class mass multiplies over disjoint unions where automorphism counts multiply). On top of those premises, gibbs_of_unit_fugacities assumes three unit normalizations of the size function at the atoms $(1,0,0)$, $(1,1,0)$, and $(1,0,1)$: the single vertex, the single loop, and the single degenerate tetrahedron.
Without those normalizations, size-blindness and gluing leave three free positive constants. The census observables $n_V$, $n_E$, $n_T$ are the vertex-, edge-, and tet-count coordinates of a complex (or ensemble). A BoundedComplex B is a complex whose labels fit in bound $B$. This definition lifts the three size-function normalizations onto an arbitrary labeled weight $w$, so the same premise can be stated either on a size function or on a labeled weight.
proof idea
Definitional Prop, not a theorem. The body is the universal quantification: for every bound $B$ and every bounded complex $K$ of that bound, if $K$ has one vertex and total incidence $n_E+n_T\le 1$, then $w,B,K=1$. No lemmas are applied; unfolding is the only step.
why it matters
This is the shared atom-normalization premise that ties the two Gap-2 derivation routes together. Downstream, unitFugacity_iff_normalizedAtTheAtoms proves unit sector fugacity on a size function is exactly this property on the corresponding size-blind weight, so "the two derivations in the library do not rest on two different premises." The same equivalence appears in the five-part fugacity_posting_gluing_verdict, which settles flag 8's premise question: unit fugacity, $\mu$ at the three atoms, and this normalization are one statement.
It also feeds no_posting_countermodel_with_nonunit_fugacity (posting $\mu$ at the atoms forces unit fugacity) and the letter-cost dichotomy side (atom_normalizations_are_derived, LetterCostDichotomyVerdict). In the module narrative, the three normalizations kill the loop-count escape while leaving the proper-edge escape open; stating them on labeled weights is what lets the posting layer be compared directly to the gluing derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.