UnitFugacity
plain-language theorem explainer
Unit sector fugacity is the predicate that a three-index size function equals one on the three atomic complexes (one vertex; one vertex plus one edge; one vertex plus one tetrahedron). Gap-2 measure constructions and the fugacity-elimination chain cite it as the residual normalization that turns the three-constant gluing residue into the Gibbs size weight. The body is a three-conjunct equality, not a derived claim.
Claim. A size function $f:\mathbb{N}^3\to\mathbb{R}$ has unit sector fugacity when $f(1,0,0)=f(1,1,0)=f(1,0,1)=1$.
background
Gap 2 asks whether the posting layer together with the carrier gluing law forces the path-sum measure down to a unique size-blind weight. The closed-form residue of gluing is three positive constants: any size-blind weight obeying the four carrier gluings is inverse gauge volume times one fugacity per index type (vertex, edge, tetrahedron), realized by the character size $u^{n_V}v^{n_E}w^{n_T}$.
The three atoms are the minimal labeled complexes with a single vertex and at most one non-vertex letter: pure vertex $(1,0,0)$, vertex-edge $(1,1,0)$, and vertex-tetrahedron $(1,0,1)$. Setting the size function to one there is exactly the hypothesis that recovers the Gibbs size weight from the three-constant family.
Non-equivariant posting already shows a continuum of costs can post the orbit-mean measure $\mu$ without fixing those constants. This module isolates the remaining question: does gluing plus posting pin the three fugacities to one?
proof idea
Definitional abbreviation only. The predicate is the conjunction of three equalities of $f$ at the atomic size triples; there is no tactic proof or lemma application.
why it matters
This flag is the residual normalization the Gap-2 measure rests on (premise flag 8 of the full-theory ledger) and the hypothesis triple behind the Gibbs-of-unit-fugacities construction. Downstream, the fugacity-elimination module uses it as the target of forcing: atom-only posting of $\mu$ plus size-weight representation yields unit fugacity; on the three-fugacity residue that is $z_V=z_E=z_T=1$; A1.7 surface purity plus kind totals land in the same elimination class with representing size function the Gibbs size.
Composition theorems then glue erasure Jacobian with unit fugacity to recover class mass equal to $\mu$ and erase the three residual constants. The module's negative result is that gluing and posting alone do not force the flag: character costs realize every positive triple while remaining kind-only and gauge-equivariant. What forces it is equivalent restatements (class mass equals $\mu$ at the atoms, or labeled weight normalized there).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.