uv_finiteness_structural
plain-language theorem explainer
The recognition path sum over admissible triangulations is UV-finite on structural grounds: the triangulation count is a positive finite bound, every admissible family has strictly positive minimum mesh, and sinh dominates the identity on nonnegative deficits. Gravity theorists citing the discrete recognition path integral against continuum EH non-renormalizability would use this. The proof is a three-component term packing positivity of the count bound, the mesh field axiom, and the standard sinh inequality.
Claim. For every admissible triangulation family $F$, the triangulation-count bound $\mathrm{growthBase}(F)^{\mathrm{maxSimplexCount}(F)}$ is strictly positive; every such $F$ has minimum mesh $\ell_{\mathrm{sub}}>0$; and for every real $\delta\ge 0$ one has $\delta\le\sinh\delta$.
background
The module treats the recognition path sum on a compact 4-manifold as a sum over admissible triangulations whose mesh is bounded below by the substrate length $\ell_{\mathrm{sub}}$:
$Z=\sum_{T:,\mathrm{mesh}(T)\ge\ell_{\mathrm{sub}}}\mu(T),\exp(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}})$.
An admissible triangulation family packages a positive maximum simplex count (from the volume/$\ell_{\mathrm{sub}}^4$ constraint), a positive growth base for a Tutte-type exponential bound on combinatorial types, and a positive minimum mesh equal to $\ell_{\mathrm{sub}}$. The triangulation count bound is then $\mathrm{growthBase}^{\mathrm{maxSimplexCount}}$, already proved positive by pow_pos on the growth base.
The third conjunct is the elementary comparison $\delta\le\sinh\delta$ for $\delta\ge 0$, which underwrites the claim that the recognition hinge weight (sinh of deficit) suppresses large curvature more strongly than the linear Regge deficit.
proof idea
Term-mode packing of three facts already on hand. The first conjunct is exactly triangulationCountBound_pos, which is pow_pos on the family's positive growth base. The second is the structure field minMesh_pos of every admissible family. The third rewrites the standard Mathlib fact Real.self_le_sinh_iff in the nonnegative direction. No new analysis is performed; the theorem is the structural certificate that these three UV ingredients hold simultaneously.
why it matters
This is the master structural certificate for UV finiteness of the recognition path sum in the Gravity domain. Continuum Einstein-Hilbert gravity is perturbatively non-renormalizable because $G$ has mass dimension $-2$ and the continuum path integral takes mesh to zero; the module argument is that those divergences are artifacts of that limit, which the recognition substrate never takes.
The three conjuncts match the module's three-part case: finite triangulation count, mesh bounded below by $\ell_{\mathrm{sub}}$, and sinh suppression of large deficits relative to Regge. Sibling results (recognition_dominates_regge, path-sum weight definitions) supply the dynamical comparison; this theorem packages the structural side with zero sorry and no RS-internal axiom. No downstream consumers are wired yet; it stands as the section's cert before any master export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.