instFintypeExactComplex
plain-language theorem explainer
For any fixed vertex, edge, and tetrahedron counts, the type of exact-size labeled combinatorial complexes is finite. Gravity path-sum arguments that need a well-defined cardinality of labeled configurations at a given signature rely on this instance. The proof is a one-line transfer of finiteness along the coding equivalence onto a product of finite function spaces.
Claim. For all $v,e,t\in\mathbb{N}$, the type of exact complexes with exactly $v$ vertices, $e$ edges and $t$ tetrahedra (incidence data $\mathrm{Fin}\,e\to\mathrm{Fin}\,v\times\mathrm{Fin}\,v$ and $\mathrm{Fin}\,t\to\mathrm{Fin}\,4\to\mathrm{Fin}\,v$) carries a finite-type structure.
background
The module builds exact complexity shells for the quotient-class path sum: configurations are grouped by exact signature $(v,e,t)$ with no size caps, then resummed under a hand-inserted Gaussian UV factor $\exp(-\rho n^2)$. An exact complex is the cap-free labeled type with incidence maps only: each edge is a vertex pair, each tetrahedron a $4$-tuple of vertices. Because there is no bound, the cross-cap identification issues of the older bounded complexes cannot arise.
Finiteness of the raw labeled type is the first Stage-1 fact needed before shells, setoids, and cardinality bounds. The coding equivalence identifies each exact complex with the product of the two incidence function spaces, both of which are finite whenever $v,e,t$ are.
proof idea
One-line wrapper. Apply Fintype.ofEquiv to the inverse of the coding equivalence, which is definitionally the pair of incidence maps. Mathlib already supplies Fintype on Fin and on function types out of finite domains, so the product type is finite and the equivalence transports that instance onto the exact-complex structure.
why it matters
Stage 1 of the Seven Gaps exact-shell program lists this finiteness among the proved facts that make the exact path class a Fintype and underwrite the shell entropy bound $\mathrm{card}\le(n+1)^{12(n+1)}$. Without a finite labeled type at each signature, the per-class measure $1/|\mathrm{Aut}|$ and the regulated shell series cannot even be stated as finite sums. The module is explicit that the regulator is mathematical, not derived physics, and that regulator removal remains an open named hypothesis; this instance only closes the combinatorial finiteness step. No continuum or mesh-refinement claim is involved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.