labeledCount_eq_card
plain-language theorem explainer
For each bound B, the natural cardinality of the type of bounded complexes equals its Fintype cardinality. Path-sum and measure arguments over the labeled class use this to switch freely between Nat.card and Fintype.card. The proof is a one-line application of the standard Mathlib identity Nat.card_eq_fintype_card.
Claim. For every natural number $B$, $\mathrm{Nat.card}(\mathrm{BoundedComplex}\,B)=\mathrm{Fintype.card}(\mathrm{BoundedComplex}\,B)$, where a bounded complex of bound $B$ is a combinatorial incidence configuration with at most $B$ vertices, edges, and tetrahedra.
background
The module builds a proved path-sum measure for the scoped Recognition Science configuration class used in gravity (Lane 2 of the Seven Gaps program). Configurations are combinatorial and equilateral at the fixed substrate mesh: geometric data lives in incidence maps, in the style of CDT and of the project's Regge triangulation type with the metric field dropped.
A bounded complex of bound $B$ packages counts $n_V,n_E,n_T\le B$ together with edge and tetrahedron incidence maps into finite vertex sets. The module already equips this type with an explicit coding equivalence, hence a Fintype instance, so both Nat.card and Fintype.card are defined and finite. This lemma only identifies the two cardinal notations.
Upstream, finiteness of the labeled class discharges the count-finiteness content that PathSumUVBound.AdmissibleTriangulationFamily had treated via a postulated growth base; the present equality is bookkeeping once that Fintype instance exists.
proof idea
One-line term proof: apply Mathlib's Nat.card_eq_fintype_card, which states that whenever a type carries a Fintype instance, its Nat.card equals Fintype.card. No local lemmas about incidence data or coding are needed; the Fintype instance on BoundedComplex B (from the coding equivalence in this module) is enough.
why it matters
The honest $Z_{RS}$ statement in this module is a finite weighted sum $Z(B,w)=\sum_K \mu(K),w(K)$ over the labeled class, with $\mu(K)=1/|\mathrm{Aut},K|$ and unitary weights $w=e^{iS}$. Norm bounds such as $|Z|\le\mathrm{card}(\mathrm{BoundedComplex},B)$ mix Nat.card and Fintype.card language; this identity makes those bounds interchangeable.
It sits under the proved tier of the module: Fintype structure on the labeled class, finite automorphism groups, positivity and relabeling invariance of $\mu$, and well-definedness of the unitary path sum. It does not close the still-open sharper exponential-growth semantics for exact simplicial subclasses (as opposed to the larger incidence superclass). No downstream dependents are recorded yet; the lemma is local glue for the measure section that follows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.