unitFugacity_iff_normalizedAtTheAtoms
plain-language theorem explainer
Unit sector fugacity for a size function is equivalent to its induced size-blind labeled weight equaling 1 on the three atomic complexes. Anyone equating the gluing and posting Gap-2 premises cites this bridge. The proof is a four-way case split on edge and tetrahedron counts forward, and three bouquet evaluations backward.
Claim. For any size function $f:\mathbb{N}^3\to\mathbb{R}$, one has $f(1,0,0)=f(1,1,0)=f(1,0,1)=1$ if and only if the labeled size-blind weight $K\mapsto\mathrm{sizeWeight}(f,K)$ equals $1$ at every atomic complex (one vertex and at most one edge or tetrahedron).
background
Gap 2 asks whether posting plus gluing can force unit sector fugacity on the path-sum measure. The gluing closed form reduces residual freedom to three positive constants (one fugacity per index type); unit sector fugacity is the hypothesis that those constants equal 1 at the three atoms $(1,0,0)$, $(1,1,0)$, $(1,0,1)$. That triple is literally the premise of the Gibbs-of-unit-fugacities construction and flag 8 of the full-theory ledger.
On the posting side, NormalizedAtTheAtoms asks that a labeled weight equal 1 on every complex with one vertex and edge-plus-tetrahedron count at most one. The size-blind weight of a size function $f$ is the labeled weight that ignores labels and reads only the three size coordinates through $f$. The module shows these two writings name the same condition once the size-blind bridge is in place.
Local setting: the module answers the open question left by the non-equivariant posting analysis, namely whether posting structural conditions together with the gluing law force the three constants to one. They do not; what forces unit fugacity is a restatement of the conclusion itself.
proof idea
Bidirectional constructor. Forward: from the three atom equalities of unit fugacity, take any bounded complex $K$ with one vertex and $n_E+n_T\le 1$. Omega forces $n_E,n_T\in{0,1}$; the four cases rewrite the sizes and discharge against $f(1,0,0)$, $f(1,1,0)$, or $f(1,0,1)$ (the double-one case is impossible by the bound). Backward: feed the three bouquet complexes (vertex only; one edge; one tetrahedron) into the normalization hypothesis and simp through the size-weight definition to recover the three equalities.
why it matters
This is the second of the two equivalent rewritings of the Gap-2 premise (the first being unit fugacity iff class mass equals $\mu$ at the atoms). Downstream, the five-part verdict theorem packages both equivalences as clause 1: the premise, the normalization, and three instances of the conclusion are one statement. From that it follows that posting $\mu$ alone forces the premise with no gluing hypothesis.
The no-posting-countermodel theorem uses the backward direction (transported across a size-function representation) to close the charged countermodel route: any letter cost that posts $\mu$ at the atoms and whose class mass is represented by a size function already has unit fugacity. The headline no-go (gluing plus posting structural conditions do not force unit fugacity) sits beside this: the gluing law constrains only the shape of the fugacity character, not its value. Together they settle flag 8's premise question in the negative for the posting-plus-gluing route while pinning exactly what remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.