sum_fiberwise_quotient
plain-language theorem explainer
Any finite sum of an AddCommMonoid-valued function on a Fintype equals the double sum that first groups by quotient classes of a Setoid, then sums inside each labeled fiber. Gravity path-sum bookkeeping cites this as the generic fiber decomposition (T1) before collapsing class-constant weights. The proof rewrites with Finset.sum_fiberwise and identifies the filtered universe with the module's classFiber.
Claim. Let $\alpha$ be a finite type, $s$ an equivalence relation on $\alpha$, and $g:\alpha\to M$ valued in an additive commutative monoid. Then $\sum_{a\in\alpha} g(a)=\sum_{q\in\alpha/s}\sum_{a\in F_q} g(a)$, where $F_q$ is the labeled fiber $\{a\mid [a]=q\}$.
background
Module Crux-2 (Seven Gaps, path-sum pillar) runs the QUOTIENT_BOOKKEEPING protocol: rewrite the labeled path sum $Z$ as a sum over triangulation classes, with honest fiber cardinalities rather than bare $1/|\mathrm{Aut}|$ weights.
The labeled fiber classFiber s q is the Finset of all $a\in\alpha$ with $\mathrm{Quotient.mk},s,a=q$ (decidability classical, noncomputable bookkeeping). Membership is exactly quotient-map equality (mem_classFiber). The fiber cardinality is fiberCard s q.
This lemma is the generic AddCommMonoid layer beneath those gravity-specific definitions. No group action is assumed; any Setoid on a Fintype works. Downstream collapse to class-constant sums and the $Z$ pushforward both start from this identity.
proof idea
Classical mode for decidability. Rewrite the left-hand sum by Mathlib's Finset.sum_fiberwise on Finset.univ along the quotient map $\mathrm{Quotient.mk},s$. The outer sum is then over quotient classes; for each class $q$, replace the Mathlib fiber filter by classFiber s q via Finset.sum_congr and an ext on membership. The membership step is simp with mem_classFiber (filter of univ equals the fiber Finset). Values of $g$ are untouched (rfl on the summand).
why it matters
This is the module's T1 fiber decomposition: the first proved brick of class pushforward for the labeled path sum. Immediate parent sum_eq_quotient_sum_classMass collapses the inner sum when $f$ is constant on classes, yielding $\sum_a f(a)=\sum_q \mathrm{fiberCard}(q)\bullet f(q.out)$.
Headline parent Z_eq_classPushforward (T2) instantiates the same rewrite on relabelSetoid B so $Z B w=\sum_q \mathrm{classMass}(q)\cdot w(\mathrm{rep},q)$ whenever $w$ is class-constant. Module doc stresses that `classMass q=|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep},q)|)$, not bare $1/|\mathrm{Aut}|$; the fork verdict at $B=2$ (non-singleton fibers) is only meaningful once this fiberwise split is available.
Scope is PathSum.Z bookkeeping only, not the exact-shell $Z_{RS}$ quotient convention. No Recognition forcing-chain landmark (T5–T8) is claimed here; the lemma is pure finite-sum algebra feeding gravity measure structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.