pathSumUVBoundCert
plain-language theorem explainer
Packages four structural facts into a UV-finiteness certificate for the recognition path sum over admissible triangulations of a compact 4-manifold. Gravity theorists citing the discrete RS path integral (mesh ≥ ℓ_sub, sinh action) use this bundle. The body is a pure structure inhabitant: each field is discharged by an existing positivity, inequality, or domination lemma.
Claim. There exists a UV-finiteness certificate for the recognition path sum asserting: (i) every admissible triangulation family $F$ has strictly positive combinatorial count bound; (ii) every such $F$ has strictly positive minimum mesh; (iii) for all $\delta \ge 0$, $\delta \le \sinh\delta$; (iv) whenever all deficit angles of a path-sum weight $w$ are nonnegative, the Regge action of $w$ is at most the recognition action of $w$.
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 admissible triangulations of a compact 4-manifold. Status is structural: zero sorry, zero RS-internal axioms.
An admissible triangulation family carries a positive growth base and a positive minimum mesh (the substrate length $\ell_{\mathrm{sub}}$). The triangulation count bound is of Tutte type, $C^{N_{\max}}$ with $N_{\max}$ set by volume over $\ell_{\mathrm{sub}}^4$. Path-sum weights assign deficit angles to hinges; the Regge action sums those deficits, while the recognition action sums $\sinh$ of the deficits.
Upstream, triangulationCountBound_pos gives positivity of the count bound via pow_pos, and recognition_dominates_regge states that nonnegative deficits imply Regge action $\le$ recognition action by termwise comparison in a finite sum.
proof idea
One-line structure construction. Field count_finite is exactly triangulationCountBound_pos. Field mesh_positive projects the family's minMesh_pos hypothesis. Field sinh_dominates is the Mathlib fact Real.self_le_sinh_iff applied in the nonnegative direction. Field recognition_dominates is the already-proved theorem recognition_dominates_regge (unfold both actions, apply Finset.sum_le_sum, use $\delta\le\sinh\delta$ hingewise). No new analysis is performed here.
why it matters
This certificate is the concrete inhabitant that makes PathSumUVBoundCert nonempty. Downstream, pathSumUVBoundCert_inhabited is the one-line Nonempty witness ⟨pathSumUVBoundCert⟩, closing the module's structural claim.
In the Recognition framework the point is conceptual: continuum EH power-counting non-renormalizability assumes a mesh-to-zero limit at fixed metric. The RS path sum never takes that limit; mesh is bounded below by $\ell_{\mathrm{sub}}$, the triangulation count is finite, and sinh suppression is strictly stronger than Regge for large deficits. The certificate records those three pillars (plus the elementary $\delta\le\sinh\delta$ comparison) as a single named object for later gravity modules to cite without reopening the combinatorial or analytic details.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.