Equivalent
plain-language theorem explainer
Two size-bounded combinatorial complexes are equivalent precisely when a relabeling isomorphism exists between them. Anyone working the path-sum measure, automorphism weights, or the finite triangulation quotient cites this predicate. The body is a one-line Prop abbreviation: nonemptiness of the explicit Relabel structure.
Claim. For a fixed bound $B\in\mathbb{N}$ and bounded complexes $K,K'$ (at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps), $K$ is equivalent to $K'$ if and only if there exists a relabeling isomorphism $K\to K'$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{\mathrm{RS}}$ on a scoped class of combinatorial triangulations. The substrate fixes edge length at the minimum mesh, so configurations are equilateral and CDT-style: all geometry sits in incidence data.
A BoundedComplex B is a labeled complex with $n_V,n_E,n_T\le B$, edge endpoints in $\mathrm{Fin},n_V$, and tetrahedron vertex maps $\mathrm{Fin},n_T\to\mathrm{Fin},4\to\mathrm{Fin},n_V$. It mirrors the incidence shape of the 3D Regge triangulation type with the metric field dropped and an explicit size cap. The superclass is intentionally broader than strict simplicial triangulations; finiteness of the superclass still yields finiteness of every subclass.
Relabeling is the structure that witnesses a combinatorial isomorphism (bijections on vertices, edges, and tets intertwining the incidence maps). Equivalence is the Prop that such a witness exists.
proof idea
Definitional one-liner. The predicate is exactly nonemptiness of the type of relabeling isomorphisms between the two complexes: no tactics, no lemmas, no computation. Downstream refl/symm/trans build explicit identity, inverse, and composite relabelings to promote this Prop to a Setoid.
why it matters
This is the raw equivalence relation underlying the finite quotient of labeled complexes by combinatorial isomorphism. The module uses it to obtain a genuine Setoid (refl/symm/trans proved via explicit relabelings, not asserted), a finite triangulation-class quotient, and the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ as a relabeling invariant. That invariance lifts to the path sum $Z(B,w)=\sum_K \mu(K),w(K)$, including the unitary weights $w=e^{iS}$, which is the honest scoped $Z_{\mathrm{RS}}$ statement.
In the Recognition gravity stack this discharges the count-finiteness content previously postulated for admissible triangulation families, while leaving sharper exponential-growth semantics for exact simplicial subclasses open. It is local scaffolding for the measure, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.