instFintypeBoundedComplex
plain-language theorem explainer
For each size bound B, the class of bounded combinatorial complexes (at most B vertices, edges, and tetrahedra with abstract incidence data) is a finite type. Gravity and path-sum workers cite this as the proved count-finiteness replacement for the old postulated growthBase field. The proof is a one-line transfer of Fintype along the explicit equivalence with a sigma/pi code type that is finite by construction.
Claim. For every natural number $B$, the set of bounded combinatorial complexes with at most $B$ vertices, edges, and tetrahedra (equipped with abstract edge and tetrahedron incidence maps) is finite: it carries a $Fintype$ instance.
background
Lane 2 of the Seven Gaps program builds a proved path-sum measure $Z_{RS}$ over a scoped configuration class at fixed lattice scale. The substrate fixes edge length at the minimum mesh, so configurations are combinatorial and equilateral (CDT-style). Geometric data lives entirely in incidence maps.
A bounded complex of bound $B$ is a structure with counts $n_V,n_E,n_T\le B$ and maps $\mathrm{edgeVerts}:\mathrm{Fin},n_E\to\mathrm{Fin},n_V\times\mathrm{Fin},n_V$ and $\mathrm{tetVerts}:\mathrm{Fin},n_T\to\mathrm{Fin},4\to\mathrm{Fin},n_V$. It mirrors the incidence shape of a 3D Regge triangulation with the metric field dropped and an explicit size cap.
The finite code type packages the same data as a dependent sum over $\mathrm{Fin}(B+1)$ sizes with function spaces between explicit finite types, so Mathlib supplies $Fintype$ automatically. An equivalence with both inverses definitional (structure eta and proof irrelevance) identifies the two presentations.
proof idea
One-line wrapper: obtain $Fintype$ on the bounded-complex type by transporting the automatic $Fintype$ on the code type along the symmetric equivalence. Concretely, apply $Fintype.ofEquiv$ to the code type and the inverse of the encoding equivalence (encode sizes into $\mathrm{Fin}(B+1)$ and incidence maps into the corresponding function types; decode by reading the Fin values back as naturals with the bound proofs). Left and right inverses are $\mathrm{rfl}$, so no further work.
why it matters
This is the module's lead THEOREM on count-finiteness: it discharges the count-finiteness content of the assumed growthBase field of the admissible triangulation family in the UV path-sum bound, replacing a postulated finite cardinal by a proved one. Scope honesty in the module doc is explicit: the superclass carries arbitrary bounded incidence data and need not be simplicial, yet finiteness of the superclass yields finiteness of every subclass.
Downstream, the true simplicial subclass is defined as the subtype of bounded complexes satisfying the simplicial predicate; its finiteness theorem inherits directly from this instance plus decidability of the predicate. That finiteness underwrites the finite automorphism groups, the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$, and the finite path sum $Z$ with modulus bounds, i.e. the honest scoped $Z_{RS}$ statement. The sharper exponential-growth semantics of growthBase for exact simplicial classes remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.