toEquivTriple_injective
plain-language theorem explainer
A relabeling of two bounded complexes is uniquely fixed by its three index bijections on vertices, edges, and tetrahedra; the commutation witnesses are propositions. Anyone proving finiteness of Aut(K) or of the full Relabel type cites this injection. The argument destructs two relabelings, reduces equality of the forgetful triples, and substitutes.
Claim. Let $K,K'$ be bounded combinatorial complexes of size at most $B$. The forgetful map sending a relabeling $r:K\to K'$ to the triple $(r_V,r_E,r_T)$ of its vertex, edge, and tetrahedron index bijections is injective: equal triples yield equal relabelings.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ over a scoped class of bounded combinatorial triangulations. A BoundedComplex B is an incidence package with at most $B$ vertices, edges, and tetrahedra (edge and tet endpoint maps, no metric field): the substrate fixes edge length at the minimum mesh, so configurations are equilateral and combinatorial (CDT-style).
A relabeling between two such complexes is a triple of index bijections on vertices, edges, and tets together with commutation propositions asserting that the incidence maps intertwine. The forgetful map toEquivTriple drops those propositions and retains only the three equivalences. Because the dropped fields are Prop-valued, proof irrelevance makes the forgetful map the natural candidate for injectivity, and hence for finiteness of the automorphism and relabeling types once the finite product of symmetric groups is in hand.
The same pattern appears for the exact-shell (fixed $v,e,t$) complexes; this declaration is the bounded-size analogue used by the path-sum measure module.
proof idea
Tactic proof by double introduction of structured relabelings. Two five-field packages (three equivalences plus two commutation props) are introduced; equality of their images under the forgetful map is rewritten by unfolding that map and product injectivity into three component equalities. Each component is substituted, after which the two packages are definitionally equal (rfl). No external lemmas beyond Prod.mk.injEq and substitution are required; the commutation fields never need to be compared explicitly because they are propositions.
why it matters
This injection is the hinge that turns the finite product of index-permutation groups into finite automorphism and relabeling types. Downstream it discharges instFiniteAut (so $\mu(K)=1/|\mathrm{Aut},K|$ is well-defined with $0<\mu\le 1$), the extensionality lemma for relabelings, and the off-diagonal instFiniteRelabel used in ExactShellGaugePreflight gauge counting. The same pattern feeds instFiniteExactAut and regulator-removal no-go instances.
In the module's honest status list this sits under the proved tier: finite Aut and the symmetry-factor measure that makes the scoped path sum $Z B w=\sum_K \mu(K),w(K)$ a finite, relabeling-invariant sum. It does not touch the still-open exponential-growth semantics of growthBase for exact simplicial subclasses; it only supplies the count-finiteness content needed for the measure to be well-defined on the superclass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.