symm_eEquiv
plain-language theorem explainer
For a relabeling isomorphism r between two size-capped combinatorial complexes, the edge-index bijection of the inverse relabeling equals the inverse of r's edge bijection. Anyone simplifying Aut or torsor calculations over BoundedComplex cites this. The proof is pure definitional equality (rfl), registered as a simp lemma.
Claim. Let $K,K'$ be bounded complexes of bound $B$, and let $r$ be a relabeling isomorphism $K\to K'$ (bijections of vertex, edge, and tetrahedron indices commuting with incidence). Then the edge bijection of the inverse relabeling equals the inverse of the edge bijection of $r$: $(r^{-1})_{\mathrm{e}} = (r_{\mathrm{e}})^{-1}$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ on a scoped class of combinatorial triangulations. Configurations are BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps and no metric field (CDT-style equilateral mesh fixed by the substrate).
A Relabel between two such complexes is a triple of equivalences on the finite index sets (vertices, edges, tets) that intertwine edge-endpoint and tet-vertex incidence. The inverse relabeling is obtained componentwise by inverting those equivalences and rewriting the commutation identities.
This lemma isolates the edge component of that inversion. Parallel simp facts exist for the vertex and tet components; together they make inverse-relabeling rewrites automatic in automorphism and torsor arguments.
proof idea
One-line definitional proof: rfl. By construction of Relabel.symm, the edge field of the inverse is exactly r.eEquiv.symm, so the stated equality holds by reduction. The @[simp] attribute feeds that reduction into the simplifier for downstream rewrites.
why it matters
Relabeling must be a genuine equivalence relation before the quotient triangulation class and the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ are well-defined. This simp lemma is the edge half of inverse-coherence for that relation.
Downstream, torsorEquiv in ExactShellGaugePreflight (and its cap-free twin in RegulatorRemovalNoGo) builds the bijection $\mathrm{Aut},K\simeq\mathrm{Relabel}(K,K')$ by $a\mapsto a\circ r_0$ with inverse $r\mapsto r\circ r_0^{-1}$; simplifying those composites needs exactly this identity. The same pattern is mirrored for exact (uncapped) complexes in ExactShellGaugeUV.
In the module's proved tier, this supports finiteness of Aut, positivity and relabel-invariance of $\mu$, and ultimately $Z$-invariance under equivalence-preserving bijections: the honest scoped $Z_{\mathrm{RS}}$ statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.