triangulationCountBound
plain-language theorem explainer
Defines the combinatorial upper bound on admissible triangulations as growthBase raised to maxSimplexCount. Anyone citing UV finiteness of the recognition path sum uses this quantity as the finite cardinality ceiling. The body is a one-line real power of the family's growth parameters.
Claim. For an admissible triangulation family $F$ (mesh $\ge \ell_{\mathrm{sub}}$, simplex count $\le N_{\max}$), the triangulation count bound is $b^{N_{\max}}$, where $b = F.\mathrm{growthBase} > 0$ is the Tutte-type growth rate and $N_{\max} = F.\mathrm{maxSimplexCount}$ is the volume-limited maximum simplex count.
background
The module treats UV finiteness of the recognition path sum
$$Z = \sum_{T:,\mathrm{mesh}(T)\ge\ell_{\mathrm{sub}}} \mu(T),\exp\bigl(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}}\bigr)$$
over triangulations of a compact 4-manifold. Continuum EH divergences are blamed on sending mesh to zero at fixed metric; here the substrate length $\ell_{\mathrm{sub}}$ never vanishes.
An admissible triangulation family packages the discrete data: a positive maximum simplex count $N_{\max}$ (from volume over $\ell_{\mathrm{sub}}^4$), a positive growth base $b$ such that the number of combinatorially distinct triangulations with at most $N$ simplices is $\le b^N$, and a positive minimum mesh equal to $\ell_{\mathrm{sub}}$. The bound defined here is exactly that exponential ceiling $b^{N_{\max}}$.
proof idea
Pure definition: return the real power F.growthBase ^ F.maxSimplexCount. No lemmas, no tactics. Downstream positivity (pow_pos on growthBase_pos) and the structural UV certificate simply read this value.
why it matters
This is the finite-count leg of the structural UV argument. uv_finiteness_structural and the certificate PathSumUVBoundCert both require 0 < triangulationCountBound F for every admissible family, together with positive min-mesh and sinh-dominates-linear suppression. Sibling lemmas triangulationCountBound_pos and _ne_zero discharge the positivity half.
In the SevenGaps bridge, proved_count_le_structural_bound shows that the concrete Fintype cardinality of BoundedComplex B sits under this bound for the derived provedFamily, so the assumed-count interface is satisfiable with computed data. Framework role: closes the "finite triangulation count" step that, with the $\ell_{\mathrm{sub}}$ cutoff and sinh action, replaces continuum power-counting non-renormalizability of EH gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.