symm_vEquiv
plain-language theorem explainer
For an exact-size combinatorial complex, the vertex bijection of a reversed relabeling equals the inverse of the original vertex bijection. Anyone working with automorphism torsors or gauge-fixed path-sum classes on cap-free shells will cite this. The proof is pure definitional equality (rfl), tagged simp for rewriting.
Claim. Let $K,K'$ be exact complexes with the same vertex/edge/tetrahedron counts, and let $r$ be a relabeling isomorphism $K\to K'$ (bijections of index sets commuting with incidence). Then the vertex component of the inverse relabeling equals the inverse of the vertex component: $(r^{-1})_{\mathrm{V}}= (r_{\mathrm{V}})^{-1}$.
background
This module builds the quotient-class path-sum configuration space as exact complexity shells: fixed counts $(v,e,t)$ of vertices, edges, and tetrahedra, with no size caps. An ExactComplex packages incidence data edgeVerts and tetVerts only; there is no embedding into a bounded ambient class, so the cross-cap identification issues of BoundedComplex never arise.
A relabeling isomorphism between two exact complexes of equal signature is a triple of bijections on the finite index sets that intertwine incidence. The structure is defined independently of the capped PathSumMeasure.Relabel. The inverse relabeling is the componentwise inverse of those bijections (with the commuting diagrams rewritten accordingly).
The same identity already exists for bounded complexes in PathSumMeasure; this is the cap-free twin used by the exact-shell gauge and regulator-removal infrastructure.
proof idea
One-line definitional proof: rfl. By construction of the inverse field on ExactRelabel, the vertex component of r.symm is exactly r.vEquiv.symm, so the equality holds by reduction. The @[simp] attribute makes the rewrite available in later simp calls when composing or inverting relabelings.
why it matters
Exact-shell gauge fixing treats witnesses between equivalent complexes as a torsor over the automorphism group. Downstream, RegulatorRemovalNoGo.torsorEquiv builds the bijection ExactAut K ≃ ExactRelabel K K' by a ↦ a.trans r0 with inverse r ↦ r.trans r0.symm; simplifying the vertex (and edge/tet) components of those composites needs this identity. The same pattern appears in the capped preflight torsor and in the exact ExactRelabel API itself.
Within the Seven Gaps honesty protocol, this is Stage-1 shell structure only: it supports well-defined class measures and automorphism counting on exact shells. It does not touch regulator removal (HasZRSRegulatorRemoval stays open), continuum limits, or any physical action; those remain named open or RED flags per the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.