toEquivTriple
plain-language theorem explainer
Extracts the underlying triple of index bijections (vertices, edges, tetrahedra) from a relabeling isomorphism of bounded complexes, discarding the incidence-commutation proofs. Anyone proving extensionality or injectivity of relabelings, or building the total torsor of relabelings, cites this projection. The body is a one-line field tuple.
Claim. Given a relabeling isomorphism $r$ between two bounded complexes $K,K'$ (bijections of vertex, edge, and tetrahedron indices that commute with incidence), return the underlying triple $(r_V,r_E,r_T)$ of equivalences $\mathrm{Fin}\,n_V(K)\simeq\mathrm{Fin}\,n_V(K')\times\mathrm{Fin}\,n_E(K)\simeq\mathrm{Fin}\,n_E(K')\times\mathrm{Fin}\,n_T(K)\simeq\mathrm{Fin}\,n_T(K')$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of combinatorial triangulations. A BoundedComplex B is a size-capped incidence structure: at most $B$ vertices, edges, and tetrahedra, with maps edgeVerts and tetVerts, mirroring Regge 3D triangulations with the metric field dropped (CDT-style equilateral mesh at the substrate scale $\ell_{\mathrm{sub}}$).
A relabeling between two such complexes is a triple of index bijections together with propositions that those bijections commute with incidence. The commutation fields are pure propositions; the geometric content of the isomorphism lives in the three equivalences alone.
This module already shows the labeled class is finite, that relabeling is an equivalence relation, and that the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ is a relabeling invariant, so the path sum is well-defined on the quotient.
proof idea
One-line definitional projection: package the three structure fields vEquiv, eEquiv, and tEquiv of the relabeling into a product of equivalences. No lemmas are applied; the commutation hypotheses are simply not projected.
why it matters
This forgetful map is the bridge from proposition-laden relabelings to bare index permutations. Downstream, injectivity of the map yields extensionality of relabelings (two relabelings equal once their three bijections agree). The same projection appears in the exact-shell gauge UV twin and as the inverse of the total torsor relabelSigmaEquiv in the regulator-removal no-go: every pair (target, witness) recovers a unique triple. Together these close the bookkeeping needed for $\mu$-invariance and for the finite path sum $Z B w=\sum_K\mu(K),w(K)$ over the scoped class, which is the honest $Z_{\mathrm{RS}}$ statement at fixed lattice scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.