TriangulationClass
plain-language theorem explainer
Combinatorially distinct bounded triangulations at fixed scale B are the quotient of labeled incidence complexes by relabeling isomorphism. Gravity and path-sum authors cite this as the configuration space on which the symmetry-factor measure and Z_RS live. The declaration is a one-line abbreviation: the setoid quotient by the proved relabeling equivalence.
Claim. For each bound $B \in \mathbb{N}$, write $\mathrm{TriangulationClass}(B)$ for the quotient of the set of $B$-bounded labeled complexes by the equivalence relation of relabeling isomorphism (vertex/edge/tet permutation preserving incidence).
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure for $Z_{RS}$ on a scoped class of combinatorial triangulations. The recognition substrate fixes edge length at the minimum mesh, so configurations are equilateral incidence data in the style of CDT / Regge: vertex, edge, and tetrahedron counts with incidence maps, metric dropped.
The labeled objects are $B$-bounded complexes: incidence structures whose size parameters sit under a fixed natural bound $B$. Two labeled complexes are equivalent when a relabeling (explicit identity, inverse, or composite) carries one incidence structure onto the other. The module proves that this relation is a genuine Setoid (refl/symm/trans via those explicit maps), not an asserted equivalence.
The quotient by that setoid is the space of combinatorially distinct triangulations. Downstream work treats it as the carrier for class-level measures $\mu = 1/|\mathrm{Aut}|$ and for finite path sums $\sum \mu(K),w(K)$.
proof idea
Pure definitional abbreviation. The body is the standard Lean quotient Quotient (relabelSetoid B), where relabelSetoid B packages the relation Equivalent on bounded complexes together with the already-proved refl/symm/trans witnesses built from identity, inverse, and composite relabelings. No tactics and no extra lemmas at this site.
why it matters
This quotient is the configuration space for the honest scoped $Z_{RS}$ path sum: finite sums of symmetry-factor weights over combinatorially distinct geometries. It is the domain of the headline carrier equivalence in CapShellBridge, which identifies bounded quotient classes at cap $B$ with the disjoint union of exact quotient shells $0,\ldots,B$.
That bridge transports class measures (classMu_capToShell), phases (classPhase_phaseModelAtCap), and reindexes the phased capped sum to an exact-shell complexity cutoff (phasedZq_eq_exactComplexityCutoff). Without a named quotient type, those maps cannot be stated at class level.
In the broader RS gravity lane this discharges the count-finiteness content needed for an admissible triangulation family (superclass finiteness implies subclass finiteness), while the sharper exponential-growth semantics for exact simplicial classes remains open. It sits under the path-sum UV-bound interface rather than under T0–T8 forcing directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.