instFintypeSimplicialComplex
plain-language theorem explainer
For every bound B, the simplicial subclass of bounded path-sum complexes is a finite type. Anyone counting or enumerating genuine triangulations inside the SevenGaps configuration class cites this instance. The proof is a one-line subtype Fintype inheritance from the already-finite superclass once IsSimplicial is decidable.
Claim. For every natural number $B$, the type of simplicial complexes of bound $B$ (pairs $(K,\mathrm{IsSimplicial}(K))$ with $K$ a bounded incidence configuration) carries a $Fintype$ instance, so it is finite and enumerable.
background
In the SevenGaps path-sum gravity setup, BoundedComplex B is the garbage-inclusive superclass of incidence configurations with vertex, edge, and tetrahedron lists bounded by $B$. It includes genuine triangulations but also degenerate edges, multi-edges, repeated tet vertices, and tets whose 1-skeleton is incomplete.
This module carves out the true simplicial subclass by the predicate IsSimplicial: no degenerate edges, no multi-edges, four distinct vertices per tet, and skeleton closure (every tet edge appears in the edge list). Face/triangle data is not carried, so triangle closure is out of scope.
SimplicialComplex B is the subtype of bounded complexes satisfying that predicate. The superclass already has a proved Fintype instance (instFintypeBoundedComplex); finiteness of the subclass follows once the predicate is decidable.
proof idea
One-line wrapper: apply Mathlib's Subtype.fintype to the ambient Fintype on BoundedComplex B and the decidability instance for IsSimplicial. No combinatorial casework is done here; inheritance does all the work.
why it matters
Phase 0b of the full gravity theory needs a finite, non-empty pool of genuine simplicial configurations before path-sum measures and gap counting can be stated without garbage configurations. This instance supplies the finiteness half: every later cardinality or enumeration argument over SimplicialComplex B (e.g. positivity via simplicialComplex_card_pos, the one-tetrahedron witness) relies on it.
It does not itself prove positivity or exhibit a witness; those are sibling theorems. Used_by is currently empty in the graph, so it is infrastructure for the simplicial class rather than a direct parent of a named downstream theorem. Within RS gravity it is the combinatorial gate that keeps the SevenGaps configuration space finite once non-simplicial junk is filtered out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.