symm
plain-language theorem explainer
Inverse of a relabeling isomorphism between two size-bounded combinatorial complexes. Anyone building the triangulation quotient, the symmetry factor μ, or the path-sum Z_RS cites this. The construction inverts the three index equivalences and rewrites the two incidence-commutation identities via apply/symm cancellation.
Claim. If $r$ is a relabeling isomorphism from a bounded complex $K$ to $K'$ (bijections of vertex, edge, and tetrahedron index sets that commute with the edge and tet incidence maps), then there is a relabeling isomorphism from $K'$ to $K$ given by the inverses of those bijections.
background
Lane 2 of the Seven Gaps gravity work builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of combinatorial triangulations. Configurations are BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps edgeVerts and tetVerts. The substrate fixes edge length at the minimum mesh, so geometry is combinatorial and equilateral (CDT-style); the metric field of Regge triangulations is dropped.
A Relabel between two such complexes is a triple of equivalences on the finite index sets that intertwine incidence: edges map under Prod.map of the vertex bijection, and each tet corner maps under the vertex bijection. The module proves that relabeling is a genuine equivalence relation and that the quotient of labeled complexes is finite, so the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ and the weighted path sum are well-defined and relabeling-invariant.
proof idea
Term-mode structure construction. Set the three fields of the reverse Relabel to r.vEquiv.symm, r.eEquiv.symm, and r.tEquiv.symm.
For edge_comm on an edge $e$ of $K'$: apply the original edge_comm at the preimage r.eEquiv.symm e, cancel apply_symm_apply, then rewrite with Prod.map_map, symm_comp_self, and Prod.map_id to recover the reverse intertwining.
For tet_comm on tet $t$ and corner $i$: same pattern, apply original tet_comm at the preimage tet, cancel apply_symm_apply, then symm_apply_apply restores the reverse vertex map.
why it matters
Together with refl and trans, this closes the proof that relabeling is an equivalence relation (relabelSetoid), which the module lists among the fully proved theorems (zero sorry, zero new axioms). That setoid yields the finite quotient TriangulationClass B, finiteness of automorphism groups, positivity and invariance of $\mu$, and finally $Z$-relabel-invariance of the path sum.
In the Recognition gravity stack this is scaffolding for the honest scoped $Z_{\mathrm{RS}}$ statement: unitary weights $w(K)=\exp(i S(K))$ with $|w|=1$ and modulus bounds $|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}(\mathrm{BoundedComplex},B)$. It does not touch the forcing chain T0–T8 or the RCL; it is pure combinatorial measure theory for the triangulation path sum. Downstream use sites are not yet wired in this graph snapshot, but the module doc places it under the equivalence-relation block that discharges count-finiteness content previously assumed in PathSumUVBound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.