proved_count_le_structural_bound
plain-language theorem explainer
For any size cap B, the number of bounded combinatorial complexes of scale at most B is at most the structural triangulation-count bound attached to the proved admissible family. Path-sum and UV-bound arguments in the gravity lane cite this to discharge the growth-base interface with concrete finite data rather than an assumed cardinal. The proof is a short reduction to n ≤ n^{B+1} for real n ≥ 1.
Claim. For every natural number $B$, writing $N_B$ for the number of bounded combinatorial complexes with at most $B$ vertices, edges, and tetrahedra, one has $N_B \le \mathrm{triangulationCountBound}(\mathcal{F}_B)$, where $\mathcal{F}_B$ is the proved admissible triangulation family at scale $B$.
background
The module builds a proved path-sum measure for the Recognition Science partition function $Z_{RS}$ in the Seven Gaps gravity lane. Configurations are combinatorial and equilateral at the substrate mesh: a bounded complex of scale $B$ carries incidence data for at most $B$ vertices, edges, and tetrahedra (CDT-style), mirroring the shape of a 3D Regge triangulation with the metric field dropped and an explicit size cap.
That class is already shown finite by an explicit coding equivalence, so its cardinality is a concrete natural number. Upstream, PathSumUVBound supplies an admissible-family interface whose growth-base field needs a finite count bound; triangulationCountBound is the structural upper bound used there. The present statement compares the derived cardinal of the bounded class against that structural bound for the proved family.
proof idea
Unfold the structural bound to expose the power $N^{B+1}$, where $N$ is the real cardinality of the bounded class. The goal becomes $N \le N^{B+1}$. From positivity of the finite cardinal one gets $1 \le N$ by casting. Then le_self_pow₀ finishes, using that the exponent $B+1$ is nonzero (successor never zero). No geometric or simplicial lemmas are needed; the comparison is pure real arithmetic on a positive integer base.
why it matters
This is the bridge that makes the assumed-count interface of the path-sum UV bound satisfiable with derived data: the proved family carries a concrete finite cardinal that sits inside the structural triangulation-count bound. The module ledger tags this as discharging the count-finiteness content of the growth-base field of an admissible triangulation family, while leaving the sharper exponential-growth semantics for exact simplicial subclasses open.
In the broader Recognition framework it supports the honest scoped $Z_{RS}$ statement (finite path sum with unitary weights and modulus bounds) without new axioms. It does not yet feed a named parent theorem in the dependency graph, but it closes the status-ledger item that the proved count is within the structural bound, which is the prerequisite for treating the path-sum measure as UV-controlled at fixed lattice scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.