one_lt_fiberCard_edgeClass
plain-language theorem explainer
At birth-interface size B = 2, the relabeling fiber of the single-edge triangulation class contains at least two distinct labeled complexes (the directed edges AB and BA). Anyone comparing labeled path-sum Z to a pure 1/|Aut| class sum cites this count. The proof is a two-point Finset card witness: both orientations sit in the fiber and are unequal.
Claim. Let the equivalence on labeled triangulations at $B=2$ be the vertex-relabeling setoid. Write $[e_{AB}]$ for the class of the one-edge complex with directed edge $(0,1)$. Then the labeled fiber of $[e_{AB}]$ has cardinality strictly greater than $1$: both $e_{AB}$ and the opposite orientation $e_{BA}$ lie in that fiber.
background
Module Crux-2 (Seven Gaps, path-sum pillar) formalizes the class pushforward of the labeled path-sum measure $Z$. For a finite type with a setoid, sums decompose fiberwise over the quotient: when a weight is constant on classes, the class contribution is $\mathrm{fiberCard}(q)\cdot f(\mathrm{rep},q)$. Applied to PathSum, $\mathrm{classMass}(q)=\sum_{K\in q}\mu(K)$, and by the sibling identity $\mathrm{classMass}=|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ on a representative.
The relabeling setoid at fixed $B$ identifies complexes related by vertex permutation. The one-edge complexes $e_{AB}$ (edge $(0,1)$) and $e_{BA}$ (edge $(1,0)$) are related by an explicit swap relabeling, so they determine the same triangulation class, yet remain distinct as labeled objects. The module header records this as the T3 fork: the standing labeled $Z$ therefore carries $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ per class, not bare $1/|\mathrm{Aut}|$.
Scope is deliberately narrow: the detonation concerns only the labeled PathSum $Z$ of PathSumMeasure. The exact-shell quotient-first $Z_{RS}$ uses a different convention and is not contradicted.
proof idea
Term-mode proof by explicit two-element witness. First, $e_{AB}$ is in its own class fiber by reflexivity of the quotient (via the membership characterization of classFiber). Second, $e_{BA}$ is in the same fiber because Quotient.sound of the symmetric edge-swap relabeling puts $e_{BA}\sim e_{AB}$. Finset.one_lt_card then applies to the pair $(e_{BA},e_{AB})$ inside the fiber, using the already-proved inequality $e_{AB}\neq e_{BA}$. No measure or automorphism cardinality is invoked; pure setoid fiber counting.
why it matters
This is the count form of the T3 fork verdict in the Seven Gaps path-sum bookkeeping. Downstream, mu_lt_classMass_edgeClass multiplies the fiber excess by positive $\mu$ (via classMass_eq_fiberCard_mul_mu, mu_congr, mu_pos) to get the numeric separation $\mu(e_{AB})<\mathrm{classMass}([e_{AB}])$, so a path sum weighted by classMass is kernel-distinct from a pure $1/|\mathrm{Aut}|$ class sum already at $B=2$.
QuotientFirstZ consumes the same fact: Zq_eq_labeledZ_iff_fiberExcess_vanishes records that labeled $Z$ equals the quotient-first object iff the fiber excess vanishes, and quotientFirstStatus_grounded keeps the RED flag that the unconditional labeled/quotient equality is unavailable precisely because non-singleton fibers exist. In the broader RS gravity ledger this closes the honest gap between labeled and inequivalent-class conventions without claiming a contradiction with exact-shell $Z_{RS}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.