Relabel
plain-language theorem explainer
A relabeling isomorphism between two size-capped combinatorial complexes: bijections of vertex, edge, and tetrahedron indices that intertwine the incidence maps. Anyone working gauge orbits, Aut groups, or path-sum invariance under reindexing cites this. It is a pure structure packing the three equivalences and two commuting conditions; no proof body.
Claim. Fix a bound $B$ and two bounded complexes $K,K'$. A relabeling is a triple of equivalences $v:[n_V(K)]\simeq[n_V(K')]$, $e:[n_E(K)]\simeq[n_E(K')]$, $t:[n_T(K)]\simeq[n_T(K')]$ such that edge endpoints and tetrahedron vertices are preserved: $K'.\mathrm{edgeVerts}(e(i))=(v\times v)(K.\mathrm{edgeVerts}(i))$ and $K'.\mathrm{tetVerts}(t(j))_k=v(K.\mathrm{tetVerts}(j)_k)$ for all indices.
background
Lane 2 of Seven Gaps builds a proved path-sum measure $Z_{RS}$ over a scoped class of combinatorial triangulations. The carrier is BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps edgeVerts : Fin nE → Fin nV × Fin nV and tetVerts : Fin nT → Fin 4 → Fin nV. MODEL: the recognition substrate fixes edge length at the minimum mesh, so configurations are equilateral and combinatorial (CDT-style); the metric field of ReggeTriangulation3D is dropped and an explicit size cap is added.
Two labeled complexes represent the same geometric object up to index permutation precisely when such a relabeling exists. The module proves that relabeling is a genuine equivalence relation (refl/symm/trans), quotients to a finite class TriangulationClass B, and that the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is a relabeling invariant. That invariance is what lets the finite path sum $Z=\sum_K \mu(K),w(K)$ descend to gauge classes.
proof idea
Definitional structure, not a theorem. The five fields are the data of an incidence-preserving reindexing: three Equivs on the finite index types Fin nV, Fin nE, Fin nT, plus the two commuting diagrams edge_comm and tet_comm that force the target incidence maps to be the pushforwards of the source maps. Downstream code builds concrete instances (identity, inverse, composite, edge-swap) by supplying those five components; no tactics run at the structure itself.
why it matters
This is the atomic gauge arrow for the whole Lane-2 stack. Downstream, equivalent_refl packages the identity relabeling as reflexivity of the gauge relation; gaugeOrbitCard_congr and gaugeOrbitCard_pos treat orbits under this relation; autEquivToExact and exactRelabelToBounded transport the same data across the cap/exact bridge; edgeSwapRelabel supplies an explicit nontrivial example. The module doc ties the structure to the proved claims: Aut is finite and nonempty, $\mu$ satisfies $0<\mu\le 1$ and $\mu$-congruence, and $Z$ is finite with $|Z|\le\sum\mu$ and relabeling invariance. Without a concrete commuting-diagram notion of isomorphism, the symmetry-factor measure and the honest scoped $Z_{RS}$ statement cannot even be stated. Open content remains the sharper exponential-growth semantics of growthBase for exact simplicial subclasses; finiteness of the superclass is already discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.