toEquivTriple_injective
plain-language theorem explainer
An exact-complex relabeling is uniquely fixed by its three index bijections on vertices, edges, and tetrahedra; the incidence-commutation data are pure propositions. Anyone counting Aut or proving finiteness of ExactRelabel cites this injectivity. The proof is a short destruct-and-subst argument on the product of equivalences.
Claim. Let $K,K'$ be exact complexes of signature $(v,e,t)$. The forgetful map sending an exact relabeling $r:K\to K'$ to the triple $(r_V,r_E,r_T)$ of index bijections $\mathrm{Fin}\,v\simeq\mathrm{Fin}\,v$, $\mathrm{Fin}\,e\simeq\mathrm{Fin}\,e$, $\mathrm{Fin}\,t\simeq\mathrm{Fin}\,t$ is injective. Equivalently, two relabelings with the same three bijections coincide.
background
The module builds cap-free exact complexity shells for the quotient-class path sum and studies the Gaussian-UV-regulated series $\sum_n e^{-\rho n^2}Z_n$. An ExactComplex v e t is a labeled combinatorial complex with exactly $v$ vertices, $e$ edges and $t$ tetrahedra, given by incidence maps edgeVerts and tetVerts, with no size-cap inequalities (unlike BoundedComplex).
An exact relabeling is a triple of index bijections that commute with those incidence maps. The forgetful map toEquivTriple drops the commutation proofs and retains only the product of the three equivalences. Because the commutation fields are propositions, equality of relabelings reduces to equality of those bijections.
This is the exact-shell analogue of the same forgetful injectivity used for capped complexes in PathSumMeasure.
proof idea
Term-mode destructuring proof. Take two exact relabelings and an equality of their images under toEquivTriple. Unfold the forgetful map and apply product injectivity (Prod.mk.injEq) to obtain equality of the three component equivalences. Substitute those three equalities into the structure; the remaining propositional commutation fields match automatically, so rfl finishes.
why it matters
Injectivity is the hinge for gauge counting on exact shells. Downstream, ext is the corresponding extensionality lemma (equal bijections imply equal relabelings). instFiniteExactAut obtains finiteness of the automorphism group by injecting ExactAut K into the finite set of index-permutation triples. The same pattern feeds instFiniteRelabel in the preflight module and the capped analogues PathSumMeasure.ext / instFiniteAut, and appears in regulator-removal no-go scaffolding (instFiniteExactRelabel).
In the Seven Gaps program this underwrites well-defined class measures $\mu=1/|\mathrm{Aut}|$ and the shell entropy bounds used for UV-regulated path-sum convergence. It does not touch regulator removal (HasZRSRegulatorRemoval remains open) or any continuum/mesh-refinement claim; those flags stay red per the module honesty disclosures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.