PathSumUVBoundCert
plain-language theorem explainer
Certificate packing the four structural ingredients of UV finiteness for the recognition path sum: positive triangulation-count bound, positive minimum mesh, sinh dominating the identity on nonnegative reals, and recognition action dominating Regge for nonnegative deficit angles. Discrete-gravity and path-integral workers cite it when discharging UV claims. Pure structure definition; inhabitance is supplied by a separate witness.
Claim. A UV-finiteness certificate is a record of four conditions: (i) for every admissible triangulation family $F$, the triangulation-count bound is strictly positive; (ii) every such $F$ has strictly positive minimum mesh; (iii) $\delta \le \sinh\delta$ whenever $\delta \ge 0$; (iv) for every path-sum weight with nonnegative deficit angles at all hinges, the Regge action is at most the recognition action.
background
The module treats the recognition path sum over admissible triangulations of a compact 4-manifold with mesh bounded below by the substrate length $\ell_{\mathrm{sub}}$:
$$Z = \sum_{T:,\mathrm{mesh}(T)\ge\ell_{\mathrm{sub}}} \mu(T),\exp\bigl(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}}\bigr).$$
An admissible triangulation family packages a positive maximum simplex count, a positive growth base (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}}$.
A path-sum weight carries hinge deficit angles and positive hinge areas. The recognition action is $\sum_\sigma A_\sigma\sinh\delta_\sigma$; the comparison Regge action is the linear form $\sum_\sigma A_\sigma\delta_\sigma$. The continuum EH mesh$\to 0$ limit is never taken on the recognition substrate.
proof idea
No proof body: this is a structure whose four fields are propositions. Inhabitance is discharged elsewhere by wiring known facts: positivity of the triangulation-count bound, positivity of each family's minimum mesh, the standard inequality $\delta\le\sinh\delta$ for $\delta\ge 0$ (via Real.self_le_sinh_iff), and the hingewise comparison that recognition action dominates Regge action when all deficit angles are nonnegative.
why it matters
This is the master certificate type for the module's UV-finiteness claim. Downstream, a concrete witness inhabits it, and a nonempty theorem records that the certificate type is inhabited. Together they package the three structural reasons the recognition path sum stays UV-finite: finite triangulation count under the volume/mesh constraint, mesh bounded below by $\ell_{\mathrm{sub}}$, and sinh suppression of large deficit angles relative to linear Regge. In the Recognition framework this underwrites the claim that continuum perturbative non-renormalizability of Einstein-Hilbert gravity is an artifact of taking mesh to zero while holding the metric fixed, a limit the discrete recognition substrate never performs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.