classCount_le_labeledCount
plain-language theorem explainer
The number of combinatorially distinct bounded triangulations (quotient by relabeling) is at most the labeled count at the same size bound B. Anyone controlling the path-sum measure Z_RS or discharging count-finiteness for the scoped triangulation family would cite this. The proof is a one-line application of cardinality comparison along the surjective quotient map.
Claim. For every $B \in \mathbb{N}$, if $\mathcal{C}_B$ is the set of labeled bounded combinatorial complexes with at most $B$ vertices, edges, and tetrahedra, and $\sim$ is relabeling isomorphism, then the number of classes satisfies $|\mathcal{C}_B/\sim| \le |\mathcal{C}_B|$.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{RS}$ over a scoped class of combinatorial triangulations at fixed lattice scale. The substrate fixes edge length at the minimum mesh, so configurations are equilateral and CDT-style: all geometric data sits in incidence maps.
A labeled configuration is a BoundedComplex B: natural numbers $n_V,n_E,n_T \le B$ together with edge and tetrahedron incidence maps into the vertex set. Relabeling isomorphism is a genuine setoid on that type (reflexive, symmetric, transitive via identity, inverse, and composite relabelings). The quotient by that setoid is the set of combinatorially distinct triangulations at bound $B$.
The module already records that the labeled class is finite (via an explicit code equivalence to a Fintype) and that the quotient is therefore finite. The present inequality is the elementary comparison of those two cardinals.
proof idea
Term-mode one-liner. Apply Nat.card_le_card_of_surjective to the canonical quotient map $\mathcal{C}_B \to \mathcal{C}_B/\sim$. Surjectivity is Quotient.exists_rep: every class has a representative. No case analysis and no size arithmetic beyond the general fact that a surjection of types induces a $\le$ on Nat.card.
why it matters
In the module's honest status list, finiteness of the labeled superclass discharges the count-finiteness content of the assumed growthBase field of PathSumUVBound.AdmissibleTriangulationFamily, and the quotient finiteness theorem closes the unlabeled side. This lemma is the direct comparison that makes the unlabeled count no worse than the labeled one, so every modulus bound written in terms of $|\mathcal{C}_B|$ (including $|Z| \le \mathrm{card}(\mathcal{C}_B)$) automatically dominates the class count.
It sits inside the gravity path-sum lane rather than the T0–T8 forcing chain: the eight-tick and $D=3$ landmarks fix the ambient discrete geometry, while this result only organizes the configuration measure. No downstream theorems currently depend on it in the graph; it is local scaffolding for the $Z_{RS}$ well-definedness narrative. The sharper exponential-growth semantics for exact simplicial subclasses remains open, as the module states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.