classFiber
plain-language theorem explainer
Defines the labeled fiber of a quotient class: the finite set of all elements of a finite type that map to a fixed class under the quotient map of a setoid. Gravity and path-sum authors cite it when decomposing labeled sums over triangulation classes. The body is a one-line classical filter of the universe by quotient-map equality.
Claim. For a finite type $\alpha$, a setoid $s$ on $\alpha$, and a class $q$ in the quotient $\alpha/s$, the labeled fiber is the finite set $\{ a \in \alpha : [a]_s = q \}$. Decidability is classical, so the construction is noncomputable bookkeeping rather than an algorithm.
background
The module implements Crux-2 of the Seven Gaps program: class pushforward bookkeeping for the labeled path-sum measure $Z$. The protocol is quotient bookkeeping on a finite carrier with a setoid (here, relabeling equivalence of triangulations). No group action is assumed; only the quotient map and finite sums.
The labeled fiber is the set-theoretic preimage of a class under the quotient map. Downstream, its cardinality multiplies the per-representative symmetry factor $\mu = 1/|\mathrm{Aut}|$, so class mass is $|\mathrm{fiber}(q)| \cdot \mu(\mathrm{rep}, q)$, not bare $1/|\mathrm{Aut}|$ per class. That distinction is the fork the module detonates at $B=2$.
Membership in the fiber is exactly equality of quotient images; the companion lemma records that equivalence for later rewrites.
proof idea
One-line definition: filter the finite universe by the predicate that the quotient map sends the element to the given class. Noncomputable because equality in the quotient is decided classically. No lemmas are applied; the body is pure Finset.univ.filter.
why it matters
This is the carrier set behind every fiberwise identity in the module. fiberCard is its cardinality; classMass sums the labeled measure $\mu$ over it; classMass_eq_fiberCard_mul_mu collapses that sum to $|\mathrm{fiber}| \cdot \mu(\mathrm{rep})$. The T1 theorems sum_fiberwise_quotient and sum_eq_quotient_sum_classMass decompose finite sums over these fibers, and Z_eq_classPushforward rewrites the standing path-sum $Z$ as a sum of class masses times class-constant weights.
The fork verdict uses the same object: one_lt_fiberCard_edgeClass shows the one-edge class at $B=2$ has labeled fiber larger than one (both edge orientations), so $\mu < \mathrm{classMass}$ on that class. Scope is the labeled $Z$ of PathSumMeasure only, not the exact-shell quotient-sum convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.