trans_vEquiv
plain-language theorem explainer
Composition of relabeling isomorphisms acts componentwise on vertices: the vertex bijection of r then s equals the composite of the two vertex bijections. Anyone proving automorphism, torsor, or translation-hom facts for the path-sum measure cites this as a simp rule. The equality is definitional (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/tet indices commuting with incidence). Then the vertex bijection of the composite equals the composite of the vertex bijections: $(r\circ s)_V = r_V\circ s_V$.
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 complex with at most $B$ vertices, edges, and tetrahedra, carrying only incidence data (edge endpoints and tet vertex maps); the substrate fixes the mesh length, so geometry is combinatorial.
A Relabel between two such complexes is a triple of bijections on the vertex, edge, and tet index sets that commute with incidence. Composition trans stacks two relabelings; each component (including the vertex map vEquiv) is defined by composing the underlying Equivs. The module proves that relabeling is a genuine equivalence relation and that the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is a relabeling invariant, so the finite path sum respects the quotient.
This lemma is the vertex-component projection of that composition law, parallel to the same simp fact on the uncapped ExactRelabel class.
proof idea
One-line definitional wrapper: rfl. By construction, (r.trans s).vEquiv is r.vEquiv.trans s.vEquiv, so the stated equality holds by unfolding Relabel.trans. Marked @[simp] so later rw/simp steps discharge vertex-component goals automatically.
why it matters
Feeds every place that reasons about composite relabelings on the capped class. Downstream, torsorEquiv (ExactShellGaugePreflight and RegulatorRemovalNoGo) builds the bijection $\mathrm{Aut},K\simeq\mathrm{Relabel}(K,K')$ by $a\mapsto a.trans,r_0$, and needs componentwise composition to prove the inverses. translationAut_add in PathSumProbes uses it to show translation by $t+s$ is the composite of translations, packaging $\mathbb{Z}N^3\to\mathrm{Aut}$ as a monoid hom under Relabel.trans. The exact-shell UV twin carries the same simp lemma for the uncapped class. Together these close the algebraic scaffolding for $\mu$-invariance and the honest finite $Z{\mathrm{RS}}$ bounds in the module doc (no new physics constants; pure measure-class bookkeeping on the triangulation side of the gravity lane).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.