relabelSetoid

Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{RS}$ over a scoped class of combinatorial triangulations. Configurations are BoundedComplex B: at most $B$ vertices, edges, and tetrahedra, with abstract incidence maps (edge endpoints and tet vertex lists) and no metric field. The substrate fixes edge length at the minimum mesh, so the class is CDT-style and equilateral; geometry lives entirely in incidence.

Two such complexes are equivalent when a relabeling isomorphism exists between them: bijections of vertex/edge/tet index sets that intertwine the incidence data. The sibling constructors supply the identity relabeling, the inverse of a relabeling, and the composite of two relabelings. The module already records that the labeled class is finite (via an explicit coding equivalence) and that the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$ is a relabeling invariant; the present definition is the Setoid that turns equivalence into a quotient carrier.

One-line packaging: the Setoid relation is exactly the existence of a relabeling isomorphism. The equivalence-proof triple is assembled from the three sibling constructors already on the shelf. Reflexivity is the identity relabeling on $K$. Symmetry unwraps a witness $r:K\to K'$ and returns $r^{-1}$. Transitivity unwraps witnesses $r$ and $s$ and returns the composite $r;s$. No new combinatorial content is proved here; the work is the earlier construction of those three relabelings.

This Setoid is the carrier for the quotient of labeled complexes by combinatorial isomorphism, i.e. the type of combinatorially distinct triangulations at bound $B$. Downstream, class pushforward defines the fiber mass of a class as the sum of $\mu$ over the labeled fiber of this Setoid, and proves the fork identity $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot\mu(\mathrm{rep},q)$. Cap-to-shell bridges use the same quotient map to move measures and automorphism counts between the capped and exact-shell presentations.

In the module's status list this is the proved step that "relabeling isomorphism is a genuine equivalence relation (refl/symm/trans proved, not asserted)", which unlocks finiteness of the quotient and the relabeling invariance of the path sum $Z$. That invariance is what makes the honest scoped $Z_{RS}$ (unitary weights $w=e^{iS}$) well-defined on classes rather than on labeled representatives. It does not close the open exponential-growth semantics for exact simplicial subclasses; it only discharges the equivalence-relation half of the quotient story.