equivalent_of_mk_eq
plain-language theorem explainer
Equality of two bounded complexes in the relabeling quotient implies they are related by a vertex relabeling. Anyone working with class fibers, class mass, or μ-congruence on triangulation classes cites this bridge. The proof is the one-line specialization of Quotient.exact to the relabel setoid.
Claim. Let $B\in\mathbb{N}$ and let $K,K'$ be bounded complexes of bound $B$. If their images under the quotient map by the vertex-relabeling setoid coincide, then $K$ and $K'$ are relabeling-equivalent.
background
In the Seven Gaps Crux-2 path-sum layer, labeled bounded complexes are identified up to vertex relabeling. The setoid relabelSetoid B generates the quotient whose points are triangulation classes; two complexes land in the same class precisely when a permutation of vertices carries one complex onto the other.
The module's protocol is quotient bookkeeping for the labeled path sum $Z$. Class mass is defined as the sum of the labeled measure $\mu$ over the fiber of a class, and later identities need that $\mu$ (and class-constant weights) are invariant under relabeling. That invariance is stated in terms of the concrete relation Equivalent, not in terms of quotient equality, so a bridge from quotient equality to Equivalent is required.
Mathlib supplies Quotient.exact: equality of Quotient.mk images recovers setoid relatedness. This declaration is that fact specialized to the relabeling setoid on BoundedComplex B.
proof idea
One-line term proof: apply Quotient.exact to the hypothesis that the two Quotient.mk images under relabelSetoid B are equal. The setoid relation is definitionally Equivalent, so the goal is discharged with no further rewriting.
why it matters
This is the standard bridge used whenever a proof has quotient-class equality and needs the concrete relabeling relation. Downstream, classMass_eq_fiberCard_mul_mu invokes it to show $\mu$ is constant on each fiber (via mu_congr), which is the identity form of the T3 fork detector: class mass equals fiber cardinality times $\mu$ of a representative. The numeric fork verdict mu_lt_classMass_edgeClass uses the same bridge on Quotient.out_eq to compare a single labeled measure against its class mass at $B=2$.
Further parents include Z_eq_classPushforward (the T2 headline decomposing labeled $Z$ over classes), the CapShellBridge preservation lemmas for class measure and automorphism cardinality, the Freudenthal torus bound mu_torusClassMember_le, and mu_out_eq_of_mk_eq in QuotientFirstZ. Without this specialization, every such argument would re-open Quotient.exact by hand. It does not itself touch T0–T8 forcing; it is infrastructure inside the gravity path-sum quotient bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.