classMass
plain-language theorem explainer
Pushforward mass of a triangulation class equals the sum of the labeled measure μ over every labeled complex in that class's fiber under relabeling. Path-sum and Seven Gaps bookkeeping cite it as the weight multiplying class-constant observables when Z is rewritten as a sum over inequivalent classes. The body is a direct Finset sum; the identity mass = fiber cardinality times μ(rep) is proved next.
Claim. For $B \in \mathbb{N}$ and a triangulation class $q$ of bounded complexes of bound $B$, the pushforward class mass is $\sum_{K \in F(q)} \mu(K)$, where $F(q)$ is the labeled fiber of $q$ under the vertex-relabeling equivalence and $\mu$ is the labeled measure on bounded complexes. Equivalently (proved separately) this equals $|F(q)| \cdot \mu(\mathrm{rep}\, q) = |F(q)|/|\mathrm{Aut}(\mathrm{rep}\, q)|$.
background
Module Crux-2 of Seven Gaps treats the path-sum $Z$ of labeled bounded complexes and its rewrite as a sum over the quotient by vertex relabeling (protocol QUOTIENT_BOOKKEEPING). A triangulation class is an equivalence class of BoundedComplex B under the relabeling setoid. The labeled fiber of a class $q$ is the Finset of all labeled complexes mapping to $q$; its cardinality is the fiber card.
The scalar $\mu$ is the labeled measure on complexes (symmetry factor $1/|\mathrm{Aut}|$ on a representative, constant on classes by mu_congr). The standing path sum $Z$ of PathSumMeasure is a labeled sum, not an a-priori quotient sum. Generic finite-quotient lemmas already give fiberwise decomposition of any additive sum over a Fintype with a Setoid; when the summand is class-constant the fiber collapses to fiber-card times the representative value.
Local note from the module header: class mass is deliberately $|\mathrm{fiber}| \cdot (1/|\mathrm{Aut}|)$, not the bare Burnside weight $1/|\mathrm{Aut}|$ per class. That distinction is the fork the later T3 theorems detonate at $B=2$.
proof idea
Definition, not a proof. Unfolds to the Finset sum of $\mu$ over classFiber (relabelSetoid B) q. No tactics, no lemmas applied at the definition site. Downstream identity classMass_eq_fiberCard_mul_mu unfolds this sum, invokes constancy of $\mu$ on the fiber via mu_congr and equivalent_of_mk_eq, and factors out $\mu(\mathrm{Quotient.out}, q)$ times the fiber cardinality.
why it matters
T2 definition in the class-pushforward pillar. It is the weight that appears in the headline rewrite Z_eq_classPushforward: for any class-constant complex weight $w$, the labeled path sum equals $\sum_q \mathrm{classMass}(q), w(\mathrm{rep}, q)$. The companion identity classMass_eq_fiberCard_mul_mu makes the factor $|\mathrm{fiber}|\cdot\mu(\mathrm{rep})$ explicit.
That factor is the fork detector. At $B=2$, one_lt_fiberCard_edgeClass and mu_lt_classMass_edgeClass prove $\mu(\mathrm{edgeAB}) < \mathrm{classMass}([\mathrm{edgeAB}])$, so the labeled $Z$ carrying classMass per class is kernel-distinct from an inequivalent-class sum weighted only by $1/|\mathrm{Aut}|$. Scope of the detonation is PathSum.Z only; ExactShellGaugeUV's $Z_{RS}$ uses the quotient-sum convention by its own header.
Also feeds Freudenthal torus class-mass bounds and the sibling equalities zRS_eq_classPushforward. In the gravity path-sum ledger this is the bookkeeping atom that keeps labeled versus quotient conventions honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.