triangulationCountBound_ne_zero
plain-language theorem explainer
For any admissible triangulation family, the combinatorial count bound (growth base to the power of the maximum simplex count) is nonzero. Gravity path-sum arguments cite this to treat the bound as a concrete positive real usable in denominators and finiteness estimates. The proof is a one-line lift of the already-proved positivity statement via ne_of_gt.
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 the triangulation count bound $b^{N_{\max}}$ satisfies $b^{N_{\max}} \neq 0$.
background
The module develops UV finiteness of the recognition path sum on a compact 4-manifold: $Z$ sums over admissible triangulations with mesh at least the substrate length $\ell_{\mathrm{sub}}$. Finiteness rests on three pillars: a finite triangulation count, the hard mesh cutoff, and sinh suppression of large hinge deficits relative to ordinary Regge weights.
An admissible triangulation family packages the discrete data for that count: a positive maximum simplex count $N_{\max}$ (from the volume/$\ell_{\mathrm{sub}}^4$ constraint), a positive growth base $b$ (Tutte-type exponential bound on combinatorially distinct triangulations with at most $N$ simplices), and the minimum mesh. The count bound is the real $b^{N_{\max}}$.
Positivity of that bound is already recorded: $0 < b^{N_{\max}}$ follows from $b>0$ and the power map. The present statement only strengthens positivity to nonvanishing, which is the form needed when the bound appears as a nonzero scalar in estimates.
proof idea
One-line term proof. Apply ne_of_gt to the sibling positivity theorem: from $0 < \mathrm{bound}(F)$ one obtains $\mathrm{bound}(F) \neq 0$. No new arithmetic on the growth base or simplex count is required; those facts already sit inside the positivity lemma via pow_pos on growthBase_pos.
why it matters
In the recognition path-sum UV argument, the sum runs over at most exponentially many triangulations once mesh and volume fix $N_{\max}$. Treating the count bound as a concrete nonzero real lets later estimates (weights, absolute convergence, comparison to Regge) divide by or scale against that bound without a zero-denominator caveat.
This sits in the first pillar of the module's structural theorem: continuum EH power-counting divergences are artifacts of sending mesh to zero at fixed metric; the recognition substrate never takes that limit. The declaration is elementary bookkeeping rather than a forcing-chain landmark (T0–T8), but it closes a tiny positivity gap so the finite-count step is usable as a real scalar. No downstream consumers are wired yet in the graph; siblings such as sinh-dominance and uv_finiteness_structural are the natural landing zone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.