boundedComplex_card_pos
plain-language theorem explainer
For every natural bound B, the finite type of size-capped combinatorial incidence complexes is nonempty, so its cardinality is strictly positive. Path-sum and UV-bound constructions in the gravity lane cite this to discharge positivity of the growth base. The proof is a one-line appeal to Mathlib's Fintype cardinality-positivity lemma, using that the empty complex inhabits the type.
Claim. For every natural number $B$, let $\mathcal{C}_B$ be the finite set of combinatorial incidence complexes with at most $B$ vertices, at most $B$ edges, and at most $B$ tetrahedra (abstract edge and tet incidence maps, no metric). Then $0 < |\mathcal{C}_B|$.
background
Lane 2 of the Seven Gaps program builds an honest path-sum measure for the scoped Recognition Science partition function $Z_{RS}$. Configurations are CDT-style: the substrate fixes edge length at the minimum mesh, so all geometric data is combinatorial incidence. The structure of a size-capped complex records vertex/edge/tet counts $\le B$ together with maps sending each edge to a pair of vertices and each tetrahedron to four vertices; the metric field of a full Regge triangulation is dropped.
That structure is already shown to be a Fintype via an explicit coding equivalence to a finite type of codes. Nonemptiness is witnessed by the empty complex (zero vertices, edges, and tets), which meets the size bounds for every $B$. Positivity of the finite cardinal is then the elementary hinge before writing the symmetry-factor measure $\mu(K)=1/|\mathrm{Aut},K|$ and the finite path sum $Z=\sum_K \mu(K),w(K)$.
The module tags this as THEOREM content that discharges the count-finiteness part of the assumed growthBase field on an admissible triangulation family; sharper exponential-growth semantics for exact simplicial subclasses stay open.
proof idea
One-line term proof: apply Mathlib Fintype.card_pos, which reduces $0 < \mathrm{card},\alpha$ to Nonempty $\alpha$ for any Fintype $\alpha$. The empty complex supplies the inhabitant of the bounded-complex type at every $B$, so the nonempty instance resolves and the goal closes with no further casework.
why it matters
Downstream, provedFamily builds an admissible triangulation family whose growth base is the actual finite cardinal of the scoped class (a derived quantity, not a postulated exponential base); positivity of that base is exactly this theorem, cast to $\mathbb{R}$. That family feeds proved_count_le_structural_bound, the bridge showing the proved count lies under the structural triangulation-count bound of the UV interface. The campaign ledger re-anchors gap flags against such imported artifacts so the ledger cannot drift.
In framework terms this is the minimal positivity step for the honest scoped $Z_{RS}$ statement: unitary weights $w=e^{iS}$ then inherit the modulus bounds $|Z|\le\sum\mu$ and $|Z|\le\mathrm{card}$. It does not touch T5–T8 forcing, the RCL, or the mass ladder; it only makes the combinatorial measure class well-defined and finite. The module still flags as open the sharper growth law on genuine simplicial subclasses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.