trans_eEquiv
plain-language theorem explainer
Composition of relabeling isomorphisms of bounded complexes acts componentwise on edge-index bijections: the edge map of r then s equals the composite of the two edge maps. Anyone proving Aut-torsor bijections, monoid-hom laws for lattice translations, or simp-normalizing composite relabelings cites this. 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$, $s:K_2\simeq K_3$ be relabeling isomorphisms (bijections of vertex, edge, and tetrahedron indices commuting with incidence). Then the edge-index bijection of the composite relabeling $r\circ s$ equals the composite of the edge-index bijections: $(r\circ s)_E = r_E\circ s_E$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{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 maps edgeVerts and tetVerts, metric dropped because the recognition substrate fixes edge length at the minimum mesh.
A relabeling between two such complexes is a triple of bijections (vertices, edges, tets) that intertwine those incidence maps. Composition of relabelings is defined fieldwise by composing the three equivalences and transporting the commutation witnesses. The edge component of that structure is the object simplified here.
The module already proves that relabeling is a genuine equivalence relation and that the quotient of labeled complexes is finite, so the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is well-defined and relabeling-invariant. Componentwise composition lemmas are the bookkeeping layer under those facts.
proof idea
One-line definitional proof. Unfolding the composite relabeling shows that its edge field is literally r.eEquiv.trans s.eEquiv, so the equality holds by rfl. Marked @[simp] so later proofs can normalize edge components of composite relabelings without manual rewriting.
why it matters
This is infrastructure for the automorphism and measure layer of the path-sum, not a physics claim by itself. Downstream, torsorEquiv (ExactShellGaugePreflight and RegulatorRemovalNoGo) builds the bijection $\mathrm{Aut},K\simeq\mathrm{Relabel}(K,K')$ by $a\mapsto a\circ r_0$; left/right inverses need componentwise composition to match. translationAut_add uses the same package to show lattice translations form a monoid homomorphism into automorphisms under relabeling composition.
In the broader RS gravity lane, the finite path sum $Z B w=\sum_K\mu(K),w(K)$ and its relabeling invariance rest on Aut being a finite group under this composition. The lemma is the edge-slot twin of the corresponding vertex/tet simp facts and mirrors the exact (cap-free) shell version in ExactShellGaugeUV. It does not touch T0–T8 forcing, RCL, or the $\alpha$ band; it closes bookkeeping inside the proved finite-measure half of Lane 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.