there
plain-language theorem explainer
On each gauge class the posted-weight divisor is constant (it depends only on the three sizes shared by every labeled complex in the class), so it factors out of the class sum. The residual condition is purely on the numerator's class total, later called numerator mass. Gap-2 posting-cost arguments cite this to reduce "posts μ" to orbit-mean-one of the Boltzmann numerator, with no equivariance assumed. The proof is the class-function factoring identity for a finite sum.
Claim. For an arbitrary letter cost, the divisor in the posted weight is a class function: it depends only on the three sizes of the gauge class, hence is constant on every labeled complex presenting that class. It therefore factors out of the class sum, and the class mass equals that common divisor times the total of the Boltzmann numerator over the class. What remains, as the condition for posting $\mu$, is a condition solely on that numerator total (the numerator mass).
background
Gap 2 asks when a letter cost posts the measure factor $\mu$ on gauge classes of labeled complexes. The equivariant route is already closed: an equivariant cost posts $\mu$ exactly when its Boltzmann numerator $\exp(-\mathrm{historyCost})$ is identically one. The residual open case is non-equivariant costs whose orbit sum of Boltzmann factors equals the orbit count while individual terms differ.
This module answers that case in the witness direction, but first records a sharp condition that holds for every cost, equivariant or not. Posted weight is a ratio whose denominator (divisor) is built from the three sizes of the complex. Every labeled complex presenting a fixed gauge class has those same sizes, so the divisor is constant on the class. The module's classMass functional totals a weight over the labeled complexes in a class without introducing a new summation convention.
Upstream cost language is the usual Recognition J-cost on positive ratios (observer and multiplicative-recognizer costs both induce $J$), but the present identity is purely about factoring a class-constant divisor from a finite class sum.
proof idea
No tactic script is attached in the extract (empty body in the page data). Mathematically the step is immediate: on a fixed gauge class the three sizes are invariants, the divisor is a function of those sizes alone, hence constant on the finite set of labeled complexes presenting the class, and a constant factors out of a finite sum. The leftover sum is exactly the total of the Boltzmann numerator over the class. No equivariance, no positivity beyond what the weight already requires, and no new decidability hypothesis enter.
why it matters
This identity is the hinge that turns the open non-equivariant posting case from a mystery into a named condition. Downstream in the same module it feeds the statements that class mass of a posted weight equals Gibbs weight times numerator mass, that $\mu$ equals orbit cardinality times the same Gibbs weight, and therefore that posting $\mu$ is exactly numerator mass equal to orbit cardinality (orbit mean one). Equivariance is then isolated as the extra constancy that upgrades mean-one to identically-one.
With mean-one named, the module can exhibit a witness: an edge-label transposition involution (twist) that splits orbits into cancelling halves, giving a one-parameter family of non-equivariant costs that post $\mu$ with non-constant numerator. That closes Gap 2 in the witness direction inside the Seven Gaps gravity stack. Broader used-by edges touch cost-rate Euler-Lagrange rigidity and $\varphi$-ladder hierarchy facts, but the local payload is the Gap-2 posting reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.