classMass_sizeWeight_eq_mu_iff
plain-language theorem explainer
A size-blind weight has class mass equal to μ at a complex exactly when its size function matches gibbsSize at that complex's (nV,nE,nT) triple. Gap-2 fugacity and posting arguments cite this as the bridge that cancels orbit cardinality. The proof rewrites both sides via the size-weight class-mass formula and μ = orbitCard · gibbsWeight, then cancels the strictly positive orbit factor.
Claim. For any size function $f:\mathbb{N}^3\to\mathbb{R}$ and any bounded complex $K$, the class mass of the size-blind weight induced by $f$ at the gauge class of $K$ equals $\mu(K)$ if and only if $f(n_V(K),n_E(K),n_T(K))=\mathrm{gibbsSize}(n_V(K),n_E(K),n_T(K))$.
background
Gap 2 asks whether the posting layer plus the gluing law force unit sector fugacity on the residual three-constant size-blind measure left by the closed-form path-sum analysis. The residue is a size function $f$ on vertex/edge/tetrahedron counts; the size-blind weight built from $f$ assigns to each labeled complex a value depending only on those counts, and class mass averages that weight over the gauge (relabeling) orbit.
The target measure $\mu$ on a complex factors as orbit cardinality times a Gibbs weight. A companion identity identifies that Gibbs weight with the explicit size function gibbsSize. Thus comparing class mass of a size-blind weight to $\mu$ is, after canceling the common positive orbit factor, exactly comparing $f$ to gibbsSize at the complex's size triple.
The module records that gluing and structural posting conditions alone do not pin the three fugacity constants to one; the intended unit point is recovered only by restating the conclusion as $\mu$ at the atoms (or everywhere).
proof idea
First obtain strict positivity of the real orbit cardinality from gaugeOrbitCard_pos (cast to $\mathbb{R}$). Rewrite the left-hand class mass by classMass_sizeWeight, rewrite $\mu$ by mu_eq_orbitCard_mul_gibbsWeight, and replace the Gibbs weight by gibbsWeight_eq_gibbsSize. Both sides of the desired equivalence then become orbitCard times a size-function value. The forward direction cancels the nonzero orbit factor by mul_left_cancel₀; the reverse substitutes the size equality and closes.
why it matters
Doc-comment labels this the bridge: the only computation the rest of §1 needs. It turns every "class mass equals μ" hypothesis into a pointwise constraint on the size function, with orbit counts gone.
Downstream, posts_mu_forces_gibbsSize is a one-line mp application at every complex; unitFugacity_iff_mu_at_atoms specializes the same bridge to the three atoms and proves unit sector fugacity is exactly μ-posting there; characterCost_posts_mu_iff and tiltedCost_classMass_eq_classMass_gibbsSize use it to separate the character-cost countermodel from the intended unit point and to identify tilted posted mass with the Gibbs size-blind mass. erasure_and_full_posting_force_gibbsSize composes the same idea at full strength across all complexes.
In the Gap-2 narrative this pins why posting-plus-gluing do not force unit fugacity, while posting μ everywhere (or at the atoms) does: the bridge converts measure equality into gibbsSize equality, which is unit fugacity on the character residue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.