classMass_zero
plain-language theorem explainer
The class mass of the zero weight on labeled complexes vanishes on every triangulation class. Anyone building linearity or antisymmetry for class-mass pushforwards cites this as the zero axiom. The proof unfolds the fiber sum and applies the standard Finset zero-sum lemma, with both branches of the class indicator reducing to 0 = 0.
Claim. For every triangulation class $c$ of bounded complexes on the bichromatic interface $B$, the class mass of the zero weight function vanishes: $\mathrm{classMass}(0, c) = 0$, where class mass is the sum of the weight over all labeled complexes presenting $c$.
background
In the Gap 2 non-equivariant posting module, one studies whether a letter cost can post the census measure $\mu$ without being equivariant. The sharp condition is that the Boltzmann numerator has orbit mean one on each gauge class, not that it is identically one.
Class mass is the pushforward of a labeled real weight $w$ onto triangulation classes: sum $w(K)$ over all labeled bounded complexes $K$ whose relabeling class equals $c$, and zero contribution otherwise. It is the natural total weight of the labeled fiber of $c$.
The zero weight is the constant function $K \mapsto 0$. Establishing that its class mass is zero is the additive identity for the later linearity and sign-flip lemmas used when an involution (edge-letter transposition) splits an orbit into canceling halves.
proof idea
Term-mode after classical. Unfold the definition of class mass to a Finset sum over all bounded complexes of an if-then-else that returns the weight on the class fiber and zero off it. Apply Finset.sum_eq_zero: for each summand, split_ifs handles both branches, and each reduces by rfl because the weight is the constant zero (on-class) or the off-class arm is already zero.
why it matters
Feeds classMass_neg in the same module, which proves class mass of $-D$ equals the negation of class mass of $D$. That sign-flip is part of the witness machinery for non-equivariant posting: an involution twist (swap of edge letters 0 and 1) pairs labeled complexes inside a class so that a sign-valued numerator can average to one without being constantly one.
Module doc frames the open Gap 2 case as whether a non-equivariant cost can post $\mu$ with a non-constant numerator whose orbit sum still equals the orbit count. The zero and additivity lemmas for class mass are the elementary algebra that lets the witness cancel on paired fibers. Downstream, this supports the sharp equivalence that posting $\mu$ is exactly orbit-mean-one of the numerator, strictly weaker than the equivariant "identically one" route closed earlier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.