triangulationClass_finite
plain-language theorem explainer
For each bound B, the set of combinatorially distinct bounded triangulations (labeled complexes modulo relabeling) is finite. Path-sum and gauge-mass uniqueness arguments in the gravity stack cite this to justify working over classes rather than labeled configurations. The proof is a one-line application of quotient finiteness once the labeled class is known finite.
Claim. For every natural number $B$, the quotient of the labeled bounded complexes of size bound $B$ by the relabeling equivalence relation is finite: there are only finitely many combinatorially distinct bounded triangulations at that bound.
background
In the Seven Gaps Lane 2 path-sum measure module, configurations are scoped combinatorial triangulations at fixed lattice scale (CDT-style equilateral mesh). The labeled type packages incidence data (vertex, edge, and tetrahedron counts with incidence maps) under a size bound $B$. That labeled type is already a Fintype via an explicit coding equivalence, so every subclass is finite even though the ambient type may contain non-simplicial incidence data.
Relabeling isomorphism is a proved equivalence relation (reflexive, symmetric, transitive), not an asserted setoid. The quotient by that relation is the type of combinatorially distinct triangulations. Class-level path sums and gauge masses need this quotient to be finite so sums and uniqueness statements range over a finite index set.
proof idea
One-line term proof: apply Mathlib Quotient.finite to the relabeling setoid. The underscore resolves the Finite instance on the underlying labeled type, which comes from the earlier Fintype instance on bounded complexes (via the coding equivalence). No further combinatorial counting is required once labeled finiteness and the setoid are in place. A companion instance re-exports the theorem as a typeclass for downstream inference.
why it matters
This closes the quotient-finiteness step in the proved path-sum measure stack for $Z_{RS}$: after labeled finiteness and the relabel setoid, class space is finite, so automorphism-normalized sums over classes are finite sums. Downstream, gaugeCountingMass_unique quantifies over triangulation classes and forces any class-mass assignment satisfying the normalized gauge-divided counting identity to equal the orbit mass $1/|\mathrm{Aut}|$.
In the Recognition gravity program this is part of the honest scoped $Z_{RS}$ statement (unitary weights $w=\exp(iS)$ with modulus bounds). Module status is explicit that sharper exponential-growth semantics for exact simplicial subclasses remain open; the theorem only discharges count-finiteness of the combinatorial quotient, which in turn discharges the count-finiteness content formerly postulated in the admissible-family growth base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.