simplicialComplex_card_pos
plain-language theorem explainer
For every size cap B, the simplicial subclass of bounded path-sum configurations has strictly positive finite cardinality, so the restricted configuration space is nonempty. Path-sum and discrete-gravity arguments cite this to rule out a vacuous measure support after dropping non-simplicial garbage. The proof is a one-line term application of the standard Fintype positivity lemma, using the inhabited instance on the subclass.
Claim. For every natural number $B$, if $\mathcal{S}(B)$ denotes the type of bounded incidence configurations of size at most $B$ that satisfy the four simplicial conditions (no degenerate edges, no multi-edges, four distinct tet vertices, and full 1-skeleton closure), then $0 < \#\mathcal{S}(B)$.
background
In the SevenGaps path-sum stack, BoundedComplex B is the garbage-inclusive superclass of bounded incidence data: vertex, edge, and tetrahedron lists capped by B. It admits degenerate edges, repeated tet vertices, multi-edges, and tets whose 1-skeleton is missing. The module carves out the true simplicial subclass by the predicate IsSimplicial: distinct edge endpoints, edges injective as unordered pairs, four distinct vertices per tet, and every tet vertex-pair realized by an edge.
SimplicialComplex B is the subtype of bounded complexes satisfying that predicate. Finiteness is inherited from the superclass Fintype plus decidability of the predicate. The empty complex is simplicial, and the module also builds an explicit one-tetrahedron witness (four vertices, six edges, one tet) so positivity need not rest on emptiness alone. Face (triangle) data is not carried, so triangle closure is out of scope here.
proof idea
One-line term proof: apply Fintype.card_pos. That lemma needs only that the type is a Fintype and Nonempty. Both are already in place for the simplicial subtype (Fintype from the superclass plus decidable membership; Nonempty from the empty simplicial complex, and independently from the one-tet witness constructed later in the module). No case split on B and no combinatorial enumeration appear in this declaration.
why it matters
Phase 0b of the full gravity path-sum theory needs a configuration class that is both finite (for a well-defined restricted path sum) and non-vacuous. Positivity of the simplicial subclass supplies the second half: after discarding non-simplicial garbage, the measure is still supported on a nonempty set for every cap B. The module header flags that resting positivity only on the empty complex would be a vacuity risk; the subsequent one-tet witness closes that gap, while this theorem records the cardinality claim itself.
No downstream consumers are wired yet (used_by is empty), so the result is infrastructure for later path-sum measure and discrete-gravity arguments rather than a step already named in T0–T8. It does not touch J-uniqueness, phi, the eight-tick octave, or the alpha band; its role is combinatorial hygiene of the configuration space those later gravity claims will sum over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.