fiberCard
plain-language theorem explainer
Labeled fiber cardinality: for a finite type with an equivalence, count how many elements land in a given quotient class. Gravity path-sum bookkeeping cites it whenever class mass is rewritten as |fiber| times the representative symmetry factor μ. The body is a one-line Finset.card of the filtered fiber.
Claim. Let $\alpha$ be finite and $\sim$ an equivalence on $\alpha$. For a class $q\in\alpha/\sim$, the labeled fiber cardinality is $\#\{a\in\alpha:\,[a]=q\}\in\mathbb{N}$.
background
Module Crux-2 (Seven Gaps, path-sum) runs the QUOTIENT_BOOKKEEPING protocol: rewrite the labeled path-sum $Z$ as a sum over triangulation classes, with honest status tags on what is proved versus convention.
The sibling classFiber is the Finset of all $a\in\alpha$ with $\mathrm{Quotient.mk},s,a=q$, built by classical filtering of Finset.univ (noncomputable measure bookkeeping, not runtime enumeration). Fiber cardinality is simply that Finset's card.
Upstream, the same fiber object feeds the generic T1 decomposition: finite sums over $\alpha$ split as sums over quotient classes of inner sums on fibers. When the summand is constant on classes, the inner sum collapses to a multiple of the representative value, and that multiple is exactly this cardinality.
proof idea
Definition, not a proof. Unfolds to (classFiber s q).card: take the classical Finset fiber of $q$ under the setoid quotient map and return its natural-number cardinality. No lemmas are applied beyond the sibling fiber construction.
why it matters
This is the integer factor that separates labeled class mass from a naive $1/|\mathrm{Aut}|$ per class. Downstream classMass_eq_fiberCard_mul_mu (T3 fork detector, identity form) states classMass q = fiberCard(q) · μ(rep q). The count-form fork verdict one_lt_fiberCard_edgeClass shows the $B=2$ one-edge class has fiber card $>1$ (both edgeAB and edgeBA), and mu_lt_classMass_edgeClass turns that into the numeric witness $μ(\mathrm{edgeAB})<\mathrm{classMass}([\mathrm{edgeAB}])$.
T1 collapse theorems (sum_fiberwise_quotient, sum_eq_quotient_sum_classMass) use it to write $\sum_a f(a)=\sum_q \mathrm{fiberCard}(q)\bullet f(\mathrm{rep},q)$ when $f$ is class-constant. The same identity reappears for Freudenthal torus class mass. Module scope: this concerns the labeled PathSum $Z$ only, not the exact-shell quotient-sum convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.