trans_tEquiv
plain-language theorem explainer
Composition of relabeling isomorphisms of bounded complexes acts componentwise on the tetrahedron-index bijections: the tet map of r then s equals the composite of the two tet maps. Anyone proving Aut-torsor or monoid-hom laws for triangulation automorphisms cites this simp fact. The proof is pure definitional equality (rfl).
Claim. Let $K_1,K_2,K_3$ be bounded combinatorial complexes of size at most $B$, and let $r:K_1\simeq K_2$ and $s:K_2\simeq K_3$ be relabeling isomorphisms (bijections of vertex, edge, and tetrahedron indices commuting with incidence). Then the tetrahedron-index equivalence of the composite relabeling $r\circ s$ equals the composite of the two tetrahedron-index equivalences: $(r\circ s)_T = r_T\circ s_T$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ on a scoped class of combinatorial triangulations. A BoundedComplex B is a CDT-style incidence package: at most $B$ vertices, edges, and tetrahedra, with abstract edge and tet incidence maps and no metric field (the substrate fixes edge length at the minimum mesh).
A relabeling between two such complexes is a triple of index bijections (vertices, edges, tetrahedra) that intertwine the incidence maps. Composition of relabelings is defined componentwise on those three equivalences, together with the transported commutation proofs. The tetrahedron component is the field used whenever one tracks how tet labels move under Aut or under lattice translations.
The module already proves that relabeling is a genuine equivalence relation and that the path-sum measure $\mu(K)=1/|\mathrm{Aut},K|$ is relabeling-invariant; componentwise transport lemmas like this one are the algebraic glue for those invariance and torsor arguments.
proof idea
One-line term proof by rfl. By definition, the composite relabeling stores tEquiv := r.tEquiv.trans s.tEquiv, so the stated equality is definitional. Marked @[simp] so later rewrites of composite Aut or translation maps fire automatically on the tet component.
why it matters
This is infrastructure for the proved path-sum lane, not a physics claim by itself. Downstream, the Aut-torsor bijection (fix one witness $r_0$, then $a\mapsto a\circ r_0$ is $\mathrm{Aut},K\simeq\mathrm{Relabel}(K,K')$) rewrites composite tet maps via this simp lemma when discharging left/right inverses. The same pattern appears on the cap-free exact class and in the regulator-removal no-go torsor.
It also feeds the group-hom law for lattice translations: translation by $t+s$ equals the composite of the two translation automorphisms, proved by Relabel.ext and component simp lemmas including this one. That monoid package sits inside the finite Aut groups used to define the symmetry factor $\mu$ in $Z=\sum_K\mu(K),w(K)$. In the broader RS gravity story this supports the honest finite $Z_{\mathrm{RS}}$ on the bounded class (module THEOREM tier), while sharper exponential growth for exact simplicial subclasses remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.