ext
plain-language theorem explainer
Two relabeling isomorphisms between bounded complexes are equal once their vertex, edge, and tetrahedron index bijections agree. Anyone building Aut, the relabeling setoid, or path-sum invariance over labeled triangulations cites this uniqueness. The proof is injectivity of the forgetful map to the triple of equivalences, then three rewrites.
Claim. Let $K,K'$ be bounded combinatorial complexes of size bound $B$, and let $r,s$ be relabeling isomorphisms $K\to K'$ (bijections of vertex, edge, and tetrahedron indices that commute with incidence). If the three index bijections of $r$ and $s$ coincide, then $r=s$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ on a scoped class of fixed-scale combinatorial triangulations. A BoundedComplex B is an incidence package with at most $B$ vertices, edges, and tetrahedra (CDT-style: edge length fixed at the substrate mesh, metric field dropped).
A relabeling between two such complexes is a triple of index bijections (vertices, edges, tets) that intertwine the edge and tet incidence maps. The commutation conditions are propositions, so the geometric content of a relabeling lives entirely in those three equivalences.
Upstream, the forgetful map sending a relabeling to its triple of bijections is injective: distinct relabelings cannot share the same index data. That injectivity is the only nontrivial input here.
proof idea
One short tactic proof. Apply injectivity of the forgetful map from a relabeling to the product of its three index equivalences. Unfold that forgetful map, then rewrite the three hypotheses (vertex, edge, tet bijections equal). Equality of the underlying triples yields equality of the relabelings.
why it matters
Extensionality is the uniqueness half of treating relabelings as data. The module uses it (with refl/symm/trans) to make relabeling a genuine equivalence relation, form the finite quotient of triangulation classes, and define the automorphism group $\mathrm{Aut},K$ of a labeled complex. The symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ and the path sum $Z=\sum_K \mu(K),w(K)$ need well-defined Aut elements and relabeling invariance; without extensionality those objects are ill-typed as sets of structures.
This sits inside the honest (0-sorry) Z_RS package for the scoped class: finite configuration type, finite Aut, $0<\mu\le 1$, and modulus bounds on $Z$. It does not touch the still-open exponential-growth semantics for exact simplicial subclasses of growthBase. No downstream edges are wired yet; the lemma is infrastructure for the Relabel namespace itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.