trans
plain-language theorem explainer
Composition of two relabeling isomorphisms between exact-size complexes of fixed signature is again a relabeling isomorphism. Anyone building the setoid of exact complexes (or proving complexity is class-invariant) cites this. The construction is componentwise composition of the vertex, edge, and tetrahedron equivalences, with incidence commutativity recovered by rewriting.
Claim. Fix $v,e,t\in\mathbb{N}$ and exact complexes $K_1,K_2,K_3$ with those counts. If $r$ is a relabeling isomorphism $K_1\to K_2$ and $s$ is a relabeling isomorphism $K_2\to K_3$ (bijections of vertex, edge, and tetrahedron indices commuting with incidence), then the composite maps $r$ then $s$ form a relabeling isomorphism $K_1\to K_3$.
background
This module organizes the quotient-class path-sum configuration space into exact complexity shells (no size caps in the shell definition) and studies a Gaussian-UV-regularized path sum. Honesty constraints: the regulator $\exp(-\rho n^2)$ is inserted by hand; the action/phase is a free class-invariant parameter; regulator removal $\rho\to 0^+$ is explicitly open.
An exact complex of signature $(v,e,t)$ is a combinatorial complex with exactly $v$ vertices, $e$ edges, and $t$ tetrahedra, given by incidence maps $\mathrm{edgeVerts}:\mathrm{Fin},e\to\mathrm{Fin},v\times\mathrm{Fin},v$ and $\mathrm{tetVerts}:\mathrm{Fin},t\to\mathrm{Fin},4\to\mathrm{Fin},v$, with no cap inequalities. A relabeling isomorphism between two such complexes is a triple of bijections on the vertex, edge, and tetrahedron index sets that intertwine those incidence maps. The structure is defined independently of the capped PathSumMeasure.Relabel type, so cross-cap identification issues cannot arise.
proof idea
Build the composite fieldwise: vertex, edge, and tetrahedron equivalences are ordinary Equiv.trans of the two factors. For edge incidence, rewrite with Equiv.trans_apply, apply the second then first edge-commutation laws, and use Prod.map_map with Equiv.coe_trans to match the composite vertex map. For tetrahedron incidence, the same pattern: Equiv.trans_apply twice, then the two tet_comm hypotheses in order. No external lemmas beyond Mathlib equivalence algebra.
why it matters
Stage 1 of the module needs the exact-class relabeling relation to be a genuine setoid (exactSetoid), so that exact complexity shells ExactPathClass n are well-defined quotients and complexity is relabeling-invariant (complexity_congr). Reflexivity, symmetry, and this transitivity are the three legs of that setoid. Downstream shell finiteness, entropy bounds, and the regulated path-sum summability sit on top of that quotient structure. Nothing here touches continuum limits, mesh refinement, or FullTheoryLedger flags; those remain open or red per the module protocol. No forcing-chain (T0–T8) landmark is claimed by this definition alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.