mem_classFiber
plain-language theorem explainer
Membership of a labeled element in the fiber of a quotient class is equivalent to the quotient map sending that element to the class. Gravity and path-sum bookkeeping cite it whenever fiber membership must be rewritten as class equality. The proof is a three-line unfold of the filter definition plus Finset membership simplification.
Claim. Let $\alpha$ be finite, $s$ a setoid on $\alpha$, $q$ a class in the quotient $\alpha/s$, and $a\in\alpha$. Then $a$ lies in the labeled fiber of $q$ if and only if the quotient map sends $a$ to $q$: $a\in\mathrm{fiber}_s(q)\iff [a]_s=q$.
background
The module implements Crux-2 of the Seven Gaps program: class pushforward of the labeled path-sum measure $Z$. Protocol is quotient bookkeeping on a finite carrier with a setoid (here, relabeling equivalence of bounded complexes). No group action is assumed; decidability of the quotient is classical and noncomputable.
The labeled fiber of a class $q$ is the Finset of all $a\in\alpha$ with $[a]=q$, obtained by filtering the universe. That definition is the immediate upstream object. The present lemma is the membership rewrite that turns set-membership goals into quotient equalities (and conversely).
Downstream fiber sums, fiber cardinalities, and class masses all route through this characterization.
proof idea
Term-mode proof by unfolding the fiber definition (universe filtered by quotient equality), rewriting with Finset membership in a filter, then simplifying away the trivial universe-membership conjunct. No external lemmas beyond the filter API.
why it matters
This is the atomic membership bridge for the whole class-pushforward stack. It is used to prove the fiber decomposition of finite sums, the class-constant collapse to fiberCard times a representative value, the identity classMass = fiberCard · μ(rep), the headline equality of labeled $Z$ with its class pushforward, and the fork verdict that the one-edge class at $B=2$ has labeled fiber cardinality strictly greater than 1 (both edgeAB and edgeBA sit in the fiber). Without the membership rewrite, those fiber-card and mass identities cannot even state their witnesses. It is pure bookkeeping infrastructure, not a physics claim, but it underwrites the kernel fact that labeled $Z$ carries weight |fiber|·(1/|Aut|) per class rather than bare 1/|Aut|.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.