zRS_eq_classPushforward
plain-language theorem explainer
For a real action S constant on relabeling classes, the labeled path sum Z with unitary weights equals the sum over triangulation classes of classMass(q) times the unitary weight at a representative. Gravity path-sum bookkeeping cites this as the unitary specialization of the class-pushforward identity. The proof is a short refine: discharge class-constancy of unitaryWeight S from constancy of S, then apply the general weight theorem.
Claim. Fix a bound $B\in\mathbb{N}$ and a real-valued action $S$ on labeled bounded complexes of size at most $B$. If $S$ is constant on relabeling-equivalence classes, then the labeled path sum $Z_B$ with unitary weights built from $S$ equals $\sum_q m(q)\,w_S(\mathrm{rep}\,q)$, where the sum runs over triangulation classes $q$, $m(q)$ is the class mass, and $w_S$ is the unitary weight of $S$.
background
This module is Crux-2 of the Seven Gaps gravity path-sum pillar: quotient bookkeeping for the labeled path sum $Z$. Complexes are labeled up to a bound $B$; Equivalent is the relabeling setoid, and TriangulationClass B is the quotient. The measure $\mu(K)$ on a labeled complex is the usual $1/|\mathrm{Aut}|$ factor; the class mass is not that factor alone.
By the sibling identity classMass_eq_fiberCard_mul_mu, class mass equals fiber cardinality times $\mu$ at a representative: $m(q)=|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep},q)|)$. The headline T2 result states that any complex weight $w$ constant on classes pushes $Z$ forward to $\sum_q m(q),w(\mathrm{rep},q)$. Unitary weights are the Boltzmann-style complex weights built from a real action $S$; they inherit class-constancy precisely when $S$ does.
The module also records the fork fact that some fibers have cardinality $>1$ already at $B=2$ (ordered edge swap), so $m(q)$ is strictly larger than $\mu$ on those classes. That separation is scoped to the labeled $Z$ of PathSumMeasure, not to quotient-native shell sums elsewhere.
proof idea
One-step specialization of the general class-pushforward theorem. Apply Z_eq_classPushforward to the weight unitaryWeight S, leaving the class-constancy hypothesis as a goal. For equivalent labeled complexes $K\sim K'$, unfold the unitary weight and rewrite by the hypothesis that $S$ itself is constant on classes. No further measure or quotient algebra is redone here.
why it matters
Supplies the unitary instance of T2 in the Seven Gaps path-sum ledger: whenever the action is class-constant, the standing labeled $Z$ with unitary weights is exactly the class-mass pushforward. That is the form needed when the path sum is driven by a real action rather than an arbitrary complex weight.
Honest scope matches the parent identity: the right-hand side carries $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ per class, not bare $1/|\mathrm{Aut}|$. The module's fork verdict (non-singleton fiber at $B=2$) shows those two conventions already disagree numerically, so this theorem deliberately does not claim equality with an inequivalent-class sum weighted only by $1/|\mathrm{Aut}|$. No downstream consumers are wired yet; the declaration closes the unitary specialization slot in the quotient-bookkeeping protocol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.