equivalent_trans
plain-language theorem explainer
Gauge equivalence of bounded complexes is transitive: if relabeling isomorphisms witness K₁ ~ K₂ and K₂ ~ K₃, their composite witnesses K₁ ~ K₃. Anyone building the Setoid or proving orbit counts are class functions cites this. The proof is a short term elimination of the two Nonempty witnesses, composing the underlying Relabel maps.
Claim. Let $K_1,K_2,K_3$ be bounded combinatorial triangulations of size at most $B$. If there exists a relabeling isomorphism $K_1\simeq K_2$ and a relabeling isomorphism $K_2\simeq K_3$, then there exists a relabeling isomorphism $K_1\simeq K_3$.
background
In the Seven Gaps gauge-preflight module, discrete gravity configurations are BoundedComplex B: combinatorial triangulations with at most $B$ vertices, edges, and tetrahedra (equilateral CDT-style, metric dropped). Two such complexes are gauge-equivalent when a Relabel isomorphism exists between them; the predicate Equivalent is exactly the nonemptiness of that type.
PathSumMeasure postulates the symmetry factor $\mu K=1/|\mathrm{Aut},K|$. This module instead derives that factor from pure gauge counting: orbit size, pair count of (copy, witness), and the mass orbitCard/pairCount on the quotient by equivalence. For those counts to descend to classes, equivalence must be a genuine relation.
Upstream, Equivalent is defined as Nonempty (Relabel K K'), and the automorphism finiteness instance injects Aut K into a finite triple of index bijections. Transitivity is the remaining leg of the Setoid after reflexivity and symmetry via identity and inverse relabelings.
proof idea
Term-mode proof on the two Nonempty hypotheses. Eliminate $h_1$ to a concrete relabeling $r:K_1\to K_2$, eliminate $h_2$ to $s:K_2\to K_3$, then package the composite $r.trans,s$ back as a witness of Nonempty (Relabel K₁ K₃). No auxiliary lemmas beyond the Relabel composition already available on the isomorphism type.
why it matters
Closes the Setoid package for gauge equivalence so orbit and pair counts are well-defined class functions. Immediate consumer is gaugeOrbitCard_congr: the orbit cardinality is independent of representative, proved by transporting membership through equivalent_trans and equivalent_symm inside a subtype equivalence.
That congruence, with the torsor/orbit-stabilizer facts (torsorEquiv, pairCount_eq_orbitCard_mul_autCard), feeds the main derivation gaugeOrbitMass_eq_mu: the counting-defined mass equals $1/|\mathrm{Aut},K|$. Without transitivity the quotient TriangulationClass B and the representative-independent mass would not lift. In the broader RS gravity stack this is bookkeeping for the discrete path-sum measure, not a forcing-chain (T0–T8) step, but it is required scaffolding for the Seven Gaps gauge story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.