classMass_one
plain-language theorem explainer
The class mass of the constant real weight 1, evaluated on any gauge class, equals the gauge-orbit cardinality of a representative. Anyone normalizing numerator masses or checking the orbit-mean-one posting criterion cites this baseline identity. The proof is a short term application of the invariant-weight class-mass formula, followed by cancelling the unit factor.
Claim. For any bound $B$ and any bounded complex $K$, the class mass of the constant weight function $w\equiv 1$ on the gauge class of $K$ equals the real number $\lvert\mathrm{Orbit}(K)\rvert$.
background
Gap 2 asks when a letter cost posts the projector coefficient $\mu$. For equivariant costs the answer is that the Boltzmann numerator must be identically one. The non-equivariant case needs a weaker criterion: the numerator need only have orbit mean one.
Class mass is the total of a real weight over a gauge class of bounded complexes (complexes with a fixed bound $B$, quotiented by letter relabeling). The gauge orbit card of a labeled representative $K$ is the size of that class when counted with labeled carriers. The constant weight $1$ is the trivial numerator against which nontrivial Boltzmann factors are compared.
The module first records structural identities (classMass_postedWeight, $\mu$ as orbit card times Gibbs weight) that turn posting $\mu$ into the single numerical condition that numerator mass equals orbit card on every class.
proof idea
Apply the general lemma for class mass of an invariant weight to the constant function $w\equiv 1$. Invariance is immediate (rfl on every relabeling). The lemma returns orbit-card times the weight value on a representative. Simplify with the identification of class orbit card with gaugeOrbitCard K and with mul_one, leaving exactly the orbit cardinality as a real.
why it matters
This is the unit case of class mass: without it, the orbit-mean-one characterization of posting $\mu$ has no calibrated baseline. Downstream, numeratorMass_tiltedCost uses the same orbit-card target for the one-parameter tilted witness cost, proving that the twist-odd excess cancels and the surviving constant one sums to the orbit count. That witness answers the open Gap 2 question left by the equivariant posting theorem and by Gap2PostingLayerFloor: a non-equivariant cost can post $\mu$ with a non-constant numerator. The identity sits inside the gravity seven-gaps program, not the T0–T8 forcing chain itself, but it closes the measure-posting side of the cost layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.