trans_eEquiv
plain-language theorem explainer
Composition of exact-complex relabelings acts componentwise on edge-index bijections: the edge map of r then s equals the composite of the two edge maps. Anyone building Aut-torsors, monoid homs into ExactRelabel, or simp-normalizing gauge orbits on exact shells will cite it. The proof is definitional (rfl) from how ExactRelabel.trans is packaged.
Claim. Let $K_1,K_2,K_3$ be exact combinatorial complexes with the same vertex/edge/tetrahedron counts. If $r:K_1\to K_2$ and $s:K_2\to K_3$ are incidence-preserving relabeling isomorphisms, then the edge-index bijection of the composite relabeling $r\circ s$ equals the composite of the edge-index bijections of $r$ and of $s$.
background
This module builds the path-sum configuration space as exact complexity shells: complexes with fixed counts $(v,e,t)$ and no size caps. An ExactComplex stores only incidence data (edge endpoints and tetrahedron vertices). A relabeling isomorphism between two such complexes is a triple of bijections on vertex, edge, and tetrahedron index sets that intertwine those incidence maps.
Composition of relabelings is defined by composing the three bijections and transporting the commutation witnesses. The edge component is therefore an ordinary composition of equivalences Fin e ≃ Fin e. The same componentwise law already appears for the capped BoundedComplex/Relabel package in PathSumMeasure; this lemma is the exact-shell twin.
Local honesty constraints still apply: the Gaussian UV factor is a hand-inserted mathematical regulator, the phase is a free class function, and regulator removal remains an open named hypothesis.
proof idea
One-line definitional proof. ExactRelabel.trans sets the composite edge field to r.eEquiv.trans s.eEquiv by construction, so the stated equality is rfl. Marked @[simp] so later ext and torsor proofs can rewrite composite edge maps without unfolding trans.
why it matters
Feeds the exact-shell Aut-torsor: RegulatorRemovalNoGo.torsorEquiv (and the parallel preflight torsor on bounded complexes) builds left/right inverses by composing with a fixed witness and its inverse, then uses ExactRelabel.ext with component lemmas such as this one. Also supports monoid-hom style identities for translation automorphisms (translationAut_add pattern) and keeps ExactRelabel/Relabel simp sets aligned.
In the Seven Gaps gravity stack this is Stage-1 gauge bookkeeping: relabeling invariance of complexity and well-definedness of the per-class measure 1/|Aut| on exact shells. It does not touch continuum limits, physical actions, or the open HasZRSRegulatorRemoval flag; those stay red by module policy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.