classMass_add
plain-language theorem explainer
Class mass is additive under pointwise sums of real functions on labeled complexes of fixed size. Gap-2 arguments cite it when splitting a tilted letter cost into a constant piece plus a twist-odd remainder. The proof unfolds the Finset-sum definition, distributes addition over the sum, and matches the filtered summands by congruence.
Claim. Let $D,E$ be real-valued functions on bounded complexes of size $B$, and let $\mathrm{cl}$ be a triangulation (gauge) class. The mass of the pointwise sum $K \mapsto D(K)+E(K)$ over $\mathrm{cl}$ equals the sum of the two separate class masses.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor $\mu$ when its Boltzmann numerator is not identically one. The module answers in the witness direction: posting $\mu$ is exactly the condition that the numerator has orbit mean one on each gauge class, a strict weakening of being identically one.
Class mass is the real total of a function $D$ over the labeled complexes presenting a fixed triangulation class (a Finset sum, with a membership filter on the summands). It is the bookkeeping device behind classMass_postedWeight and the orbit-mean characterization of posting: the posted weight's class mass factors as a Gibbs weight times the numerator total over the class.
Additivity of that total in $D$ is the elementary linearity step used before introducing the twist involution (edge-letter swap $0\leftrightarrow 1$) that splits orbits into cancelling halves.
proof idea
Term-mode proof under classical logic. Unfold the definition of class mass to a Finset sum. Rewrite by the reverse of Finset.sum_add_distrib so the sum of pointwise sums becomes a sum of sums. Finish with Finset.sum_congr: on each summand, split_ifs handles the membership filter and simp equates the filtered values of $D+E$ with those of $D$ and $E$. No external lemmas beyond the Finset library are required.
why it matters
Linearity is the first algebraic property of class mass in the non-equivariant posting module. Downstream, classMass_neg is obtained by applying this theorem to $D$ and $-D$ and using the zero case, so signed remainders are well-defined.
That signed calculus feeds numeratorMass_tiltedCost: for the one-parameter tilted witness cost, the excess of the numerator over one is twist-odd, hence cancels in the class sum, leaving numerator mass equal to the orbit count. That is exactly the orbit-mean-one criterion for posting $\mu$ without an identically-one numerator.
In the broader Seven Gaps gravity stack this closes the open case left by the equivariant posting theorem: equivariance forced constancy on orbits; without it, mean one still holds for a concrete family. The result is pure measure bookkeeping on gauge classes, not a new forcing-chain step (T0–T8), but it discharges the Gap-2 witness direction named in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.