Z_eq_classPushforward
plain-language theorem explainer
For any weight constant on relabeling classes, the labeled path sum Z equals the sum over triangulation classes of classMass(q) times the weight at a representative. Gravity path-sum bookkeeping cites this as the T2 class-pushforward identity. The proof unfolds Z, applies the generic fiberwise quotient sum, then collapses each fiber using class-constancy of w and the definition of classMass.
Claim. Fix a bound $B\in\mathbb{N}$ and a weight $w$ on labeled bounded complexes that is constant on relabeling-equivalence classes. Then the labeled path sum equals its class pushforward: $Z(B,w)=\sum_{q}\mathrm{classMass}(q)\,w(\mathrm{rep}\,q)$, where the sum runs over triangulation classes $q$ and $\mathrm{rep}\,q$ is any chosen representative.
background
This module is Crux-2 of the Seven Gaps gravity pillar: path-sum quotient bookkeeping. The standing object is the labeled path sum $Z(B,w)$ from PathSumMeasure, a finite sum over labeled bounded complexes $K$ of $\mu(K),w(K)$. Here $\mu(K)$ is the labeled symmetry weight $1/|\mathrm{Aut}(K)|$, and complexes are identified up to vertex relabeling via the setoid relabelSetoid.
A triangulation class $q$ is a point of the quotient. Its fiber is the set of labeled complexes mapping to $q$; classMass q is the sum of $\mu$ over that fiber. By the sibling identity classMass_eq_fiberCard_mul_mu, this equals $|\mathrm{fiber}(q)|\cdot\mu(\mathrm{rep},q)$, not bare $1/|\mathrm{Aut}|$ per class.
The generic upstream lemma FiniteQuotient.sum_fiberwise_quotient decomposes any finite sum over a type along the fibers of a setoid quotient. When the summand is constant on classes, the fiber collapses to a multiple of the value at a representative. That is the algebraic engine behind the present identity.
proof idea
Unfold the definition of $Z$. Rewrite the labeled sum via FiniteQuotient.sum_fiberwise_quotient applied to the setoid and the summand $K\mapsto(\mu K:\mathbb{C})\cdot w K$, obtaining a sum over classes of fiber sums.
For each class $q$, every $K$ in the fiber is equivalent to Quotient.out q (via equivalent_of_mk_eq and mem_classFiber). The hypothesis that $w$ is class-constant therefore replaces $w K$ by $w(\mathrm{out},q)$ throughout the fiber. Factor the common complex factor out of the sum (Finset.sum_mul), leaving $(\sum_{K\in\mathrm{fiber}}\mu K)\cdot w(\mathrm{out},q)$. Unfold classMass and coerce the real fiber sum of $\mu$ into $\mathbb{C}$ to finish.
why it matters
This is the headline T2 theorem of the class-pushforward module: it converts the labeled path sum into an explicit sum over inequivalent triangulation classes weighted by class mass. Downstream, zRS_eq_classPushforward is the unitary special case (class-constant real action $S$, weight $e^{iS}$), obtained as a one-line application of this result. labeledZ_eq_sum_fiberCard_mul_mu in QuotientFirstZ further rewrites the same identity with the fiber-cardinality factor written out, bridging to quotient-first conventions.
The honest scope is framework-critical. The module detonates the C1 landmine as a kernel fact: at $B=2$, fibers need not be singletons, so classMass carries $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ and differs from a pure $1/|\mathrm{Aut}|$ class sum (mu_lt_classMass_edgeClass). This concerns only the labeled $Z$ of PathSumMeasure; the exact-shell $Z_{RS}$ uses a different quotient-sum convention and is not contradicted. In the broader RS gravity stack this keeps path-sum measure bookkeeping aligned with the labeled ledger before continuum or phenomenological limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.