gibbsSize_unitFugacity
plain-language theorem explainer
The Gibbs size function equals one at the three atoms (one vertex and at most one incidence). Gap-2 fugacity elimination and any argument that treats unit sector fugacity as the gluing-derivation premise cite this. The proof is a three-conjunct term that applies the atom-size evaluation lemma thrice under numeric normalization.
Claim. The Gibbs size function $s:\mathbb{N}^3\to\mathbb{R}$ satisfies unit sector fugacity: $s(1,0,0)=1$, $s(1,1,0)=1$, and $s(1,0,1)=1$. Equivalently, $s$ is normalized on the three atomic complexes (one vertex; empty, one edge, or one tetrahedron).
background
Gap 2 asks whether posting plus gluing 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); the measure is recovered once those constants equal one at the atoms. Unit sector fugacity is exactly that triple: a size function $f$ with $f(1,0,0)=f(1,1,0)=f(1,0,1)=1$, the hypothesis of the carrier-shuffle Gibbs reconstruction and ledger flag 8.
The Gibbs size function is the reciprocal of the product of factorials of the three size counts. Its labeled Gibbs weight is the same reciprocal, so evaluating size at the atoms is evaluating the weight on the three atomic complexes. The module's load-bearing equivalence later says unit fugacity holds for any size function iff class mass of the size-blind weight equals the projector scalar $\mu$ at those atoms; the present fact is the concrete witness that Gibbs size itself sits on the unit side.
proof idea
Term-mode constructor for the three conjuncts of UnitFugacity. Each conjunct is gibbsSize_eq_one_at_atom_sizes applied to a numeric side condition discharged by norm_num (the three atom size triples). No gluing, posting, or class-mass reasoning enters; the identity is pure evaluation of the factorial formula at $(1,0,0)$, $(1,1,0)$, and $(1,0,1)$.
why it matters
This is the free conjunct in the A1.7 widening: once surface purity and fixed kind totals force the posted weight to equal size-weight of Gibbs size, unit fugacity of Gibbs size needs no binders (unit_fugacity_forced_by_surface_and_kindTotals). Hostile probes re-export it as the hypothesis-free witness (gibbsSize_witnesses_unit_fugacity, a17_lands_ignores_binders) and as the first conjunct of the elimination verdict.
Downstream, three_fugacities_collapse_via_characterCost and fugacity_elimination_verdict use it when collapsing the three-fugacity residue to $(1,1,1)$ under atom posting of $\mu$. In the Gap-2 story it separates what is automatic (Gibbs size is already unit-fugacity) from what must still be forced (that a general posted weight is size-weight of Gibbs size). It does not close the open negative: gluing plus posting alone still fail to force unit fugacity for arbitrary character sizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.