symm_tEquiv
plain-language theorem explainer
For a relabeling isomorphism r between two size-capped combinatorial complexes, the tetrahedron-index bijection of the inverse relabeling equals the inverse of r's tetrahedron-index bijection. Anyone simplifying Aut or Relabel compositions in the path-sum measure cites this. The proof is pure definitional equality (rfl), registered as a simp lemma.
Claim. Let $K,K'$ be bounded combinatorial complexes of size at most $B$, and let $r$ be a relabeling isomorphism $K\to K'$ (bijections of vertex, edge, and tetrahedron index sets commuting with incidence). Then the tetrahedron-index component of $r^{-1}$ equals the inverse of the tetrahedron-index component of $r$: $(r^{-1})_{\mathrm{tet}} = (r_{\mathrm{tet}})^{-1}$.
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 CDT-style configuration with at most $B$ vertices, edges, and tetrahedra, carrying only incidence data (edge endpoints and tet vertex maps); the substrate fixes the edge length at the minimum mesh, so geometry is combinatorial.
A relabeling between two such complexes is a triple of index bijections (vertices, edges, tetrahedra) that commute with those incidence maps. The tetrahedron component is the equivalence $r_{\mathrm{tet}}:\mathrm{Fin},n_T(K)\simeq\mathrm{Fin},n_T(K')$. Inverse and composition of relabelings are defined componentwise on these equivalences, so identities such as this one are expected by construction.
The module already proves that relabeling is a genuine equivalence relation and that the quotient of labeled complexes is finite, which feeds the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ and the finite path sum $Z=\sum_K\mu(K),w(K)$.
proof idea
One-line definitional proof: both sides reduce to the same term under the structure definition of inverse relabeling, so rfl closes the goal. The declaration is marked @[simp] so tactic automation rewrites tetrahedron components of inverse relabelings without manual unfolding.
why it matters
This is bookkeeping infrastructure for the relabeling groupoid on the capped triangulation class. Downstream, the torsor equivalence in ExactShellGaugePreflight (and its cap-free twin in RegulatorRemovalNoGo) builds bijections $\mathrm{Aut},K\simeq\mathrm{Relabel}(K,K')$ by composing with a fixed witness and its inverse; simp needs componentwise identities like this one when discharging left_inv/right_inv via Relabel.ext.
It also mirrors the identical lemma on the uncapped ExactRelabel type in ExactShellGaugeUV, keeping the capped and exact shells aligned. Within the module status list, it supports the proved claims that relabeling is an equivalence, $\mu$ is relabeling-invariant, and $Z$ is invariant under equivalence-preserving bijections of configurations: the honest scoped $Z_{\mathrm{RS}}$ statement. No forcing-chain landmark (T5–T8) is touched; this is pure combinatorial measure hygiene for the gravity path sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.