tiltedCost_classMass_eq_classMass_gibbsSize
plain-language theorem explainer
For every tilt parameter with absolute value less than one, every bound, and every bounded complex, the class mass of the tilted cost's posted weight equals the class mass of the size-blind Gibbs weight. Gravity and Gap-2 measure theorists cite it to identify the tilted family's orbit-level mass with the unit-fugacity Gibbs mass. The proof rewrites via the tilted family's mu-posting lemma, then applies the size-weight/mu characterization of Gibbs class mass.
Claim. Fix $t\in\mathbb{R}$ with $|t|<1$, a bound $B'$, and a bounded complex $K$ of that bound. The class mass of the posted weight of the tilted letter cost at parameter $t$, evaluated on the relabeling class of $K$, equals the class mass of the size-blind weight built from the Gibbs size function on that same class.
background
Gap 2 asks whether the posting layer together with the carrier gluing law forces unit sector fugacity for the path-sum measure. The residual freedom after gluing is three positive constants (one fugacity per index type); unit fugacity is the premise that sets them all to one and recovers the Gibbs measure.
The prior module produced a continuum of non-equivariant letter costs (the tilted family, $|t|<1$) that still post $\mu$: posting $\mu$ means the orbit mean of the Boltzmann numerator equals one, equivalently the posted weight's class mass agrees with $\mu$. Separately, the size-blind Gibbs weight is exactly the weight whose class mass is $\mu$ at every class, realized by the size function gibbsSize.
Class mass is the orbit-level mass on the quotient by the relabeling setoid. Size-blind weights factor through a size function on complexes; the Gibbs size function is the unit-fugacity choice in that family.
proof idea
Two-step term proof. First rewrite the left-hand side by the lemma that the tilted cost posts $\mu$ (under $|t|<1$), so its posted class mass is $\mu$ on the class of $K$. Second, apply the characterization that the class mass of the size-blind Gibbs weight equals $\mu$ on every class (the reverse direction of that iff, at the reflexive witness), and symmetrize the equality. No induction or case split.
why it matters
This is the identification step that lets the tilted family serve as a positive exhibit rather than a countermodel at class-mass level. The immediate parent is the gluing-with-unit-fugacity theorem for the tilted family: once class mass equals the Gibbs class mass, and Gibbs size both glues and has unit fugacity, the tilted posted class mass inherits gluing and unit fugacity at every cap and complex.
In the Gap-2 narrative that answers whether posting plus gluing force unit fugacity, the character-cost family shows the answer is no in general (fugacity can be any positive character). The tilted family shows the complementary point: underdetermination from non-equivariant tilting lives only at the labeled level, below class mass, where carrier shuffle cannot see it. The charged first step is therefore forced, not accidental: posting $\mu$ is agreeing with Gibbs class mass, and Gibbs size is already unit.
It also feeds the index flag that unit fugacity is not shown underivable from posting alone in the sense recorded by that boolean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.