trans
plain-language theorem explainer
Composite of two relabeling isomorphisms between size-bounded combinatorial triangulations is again a relabeling. Anyone assembling the quotient of labeled complexes by combinatorial isomorphism, or the symmetry-factor path-sum measure, cites this. The construction composes the three index bijections and discharges incidence commutation by rewriting along Equiv.trans.
Claim. Let $K_1,K_2,K_3$ be bounded combinatorial complexes of size at most $B$. Given relabeling isomorphisms $r:K_1\simeq K_2$ and $s:K_2\simeq K_3$ (bijections of vertex, edge, and tetrahedron indices that commute with the edge- and tet-incidence maps), the composite $s\circ r$ is a relabeling isomorphism $K_1\simeq K_3$.
background
The module builds a proved path-sum measure for the scoped Recognition Science partition function $Z_{RS}$ over bounded combinatorial triangulations (Seven Gaps, Lane 2). Configurations live in BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps edgeVerts and tetVerts. The substrate fixes edge length at the minimum mesh, so geometry is combinatorial and equilateral (CDT-style); the structure mirrors Regge triangulation incidence with the metric field dropped and an explicit size cap.
A relabeling between two such complexes is a triple of bijections on the vertex, edge, and tet index sets that intertwine the incidence maps: edges push forward under the product of the vertex map, and each tet corner is sent by the vertex map. Reflexivity, symmetry, and transitivity of this relation are proved (not postulated), so the quotient of labeled complexes is well-defined and finite.
The parameter $B$ in the signature is the size bound on the complex; the cosmology import of the same name is unrelated interface data and is not used in the body.
proof idea
Term-mode structure construction. Set the three index equivalences to the ordinary composition of Equivs: vertex, edge, and tet maps of $r$ followed by those of $s$.
The two commutation fields are discharged by short rw scripts. For edges: unfold Equiv.trans on the composite edge map, apply $s$'s then $r$'s edge-commutation, push the product map through Prod.map_map, and reassociate the vertex composite. For tets: the same pattern on each corner index, using Equiv.trans_apply twice around the two tet_comm hypotheses. No external lemmas beyond Mathlib Equiv API.
why it matters
This is the third leg of the equivalence-relation package for combinatorial isomorphism of bounded complexes (with refl and symm). The module doc records the target: relabeling is a genuine equivalence (relabelSetoid), the quotient TriangulationClass B is finite, the automorphism group of a labeled complex is finite and nonempty, and the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ is a relabeling invariant. Those facts underwrite the finite path sum $Z(B,w)=\sum_K \mu(K),w(K)$ and its modulus bounds, including the unitary instance $w=e^{iS}$ that gives the honest scoped $Z_{RS}$ statement.
No downstream edges are recorded yet in the graph, but the declaration is load-bearing scaffolding for every invariance claim that descends through the quotient. It does not touch the forcing chain (T0–T8) or the RCL directly; it closes combinatorial bookkeeping inside the gravity path-sum lane so that count-finiteness of the configuration class is proved rather than assumed via growthBase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.