triangulationCountBound_pos
plain-language theorem explainer
For any admissible triangulation family, the combinatorial count bound growthBase^N is strictly positive. UV-finiteness arguments for the recognition path sum cite this to guarantee a finite, nonzero upper bound on the number of mesh-admissible triangulations. The proof is a one-line application of real-power positivity to the family's positive growth base.
Claim. Let $F$ be an admissible triangulation family (mesh bounded below by $\ell_{\mathrm{sub}}$, simplex count at most $N_{\max}$, combinatorial growth base $b>0$). Then $0 < b^{N_{\max}}$.
background
The module establishes UV finiteness of the recognition path sum over admissible triangulations of a compact 4-manifold. The sum is restricted to triangulations with mesh at least $\ell_{\mathrm{sub}}$ and simplex count capped by the volume constraint $N_{\max}=V/\ell_{\mathrm{sub}}^4$.
An admissible triangulation family packages those constraints: a positive maximum simplex count, a positive growth base $b$ such that the number of combinatorially distinct triangulations with at most $N$ simplices is $\le b^N$ (Tutte-type bound), and a positive minimum mesh. The triangulation count bound is the concrete real $b^{N_{\max}}$.
Positivity of that bound is the first structural ingredient in the module's three-part finiteness argument (finite count, mesh cutoff, sinh suppression of large deficits).
proof idea
One-line term proof. The bound is defined as growthBase ^ maxSimplexCount. Apply Mathlib pow_pos to the structure field growthBase_pos : 0 < growthBase; the exponent is irrelevant once the base is positive.
why it matters
This is the positivity half of the finite-count leg of UV finiteness. Downstream, uv_finiteness_structural packages it as the first conjunct ($\forall F,, 0 < b^{N_{\max}}$), and pathSumUVBoundCert records it as count_finite. The sibling triangulationCountBound_ne_zero is the immediate corollary via ne_of_gt.
In the Recognition framework this closes the combinatorial side of the claim that continuum EH power-counting divergences are artifacts of sending the mesh to zero while holding the metric fixed. The substrate never takes that limit: mesh $\ge \ell_{\mathrm{sub}}$ and the triangulation set is finite, so the path sum has no UV divergence from unbounded simplex refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.