pathSumUVBoundCert_inhabited
plain-language theorem explainer
The UV-finiteness certificate for the recognition path sum is inhabited: a concrete witness packages finite triangulation growth, positive substrate mesh, sinh-versus-linear domination, and recognition-over-Regge action comparison. Gravity theorists citing the structural UV bound use this existence fact. The proof is a one-line term that supplies the assembled certificate definition as the Nonempty witness.
Claim. There exists a UV-finiteness certificate for the recognition path sum: a record asserting that every admissible triangulation family has a strictly positive combinatorial count bound and a strictly positive minimum mesh, that $\delta \le \sinh\delta$ for all $\delta \ge 0$, and that the recognition action dominates the Regge action whenever all deficit angles are nonnegative.
background
The module treats UV finiteness of the recognition path sum on a compact 4-manifold. Configurations are admissible triangulations whose mesh is bounded below by the substrate length $\ell_{\mathrm{sub}}>0$. The formal sum is $Z=\sum_T \mu(T),\exp(i S_{\mathrm{RS}}(T)/\hbar_{\mathrm{RS}})$ over those triangulations.
The certificate structure packages four structural claims: (i) the Tutte-type count bound on combinatorially distinct triangulations with at most $N_{\max}=V/\ell_{\mathrm{sub}}^4$ simplices is strictly positive; (ii) every admissible family has positive minimum mesh; (iii) $\sinh$ weakly dominates the identity on $[0,\infty)$; (iv) for nonnegative deficit angles the recognition action (built from $\sinh$ of deficits) is at least the Regge action (linear in deficits). Together these block the continuum mesh$\to 0$ limit that produces Einstein-Hilbert power-counting divergences.
Upstream, the concrete certificate definition fills the four fields from the positivity of the triangulation count bound, the family's mesh positivity hypothesis, the real-analysis fact $\delta\le\sinh\delta$ for $\delta\ge 0$, and the in-module comparison that recognition dominates Regge.
proof idea
One-line term proof. Nonemptiness of the certificate type is witnessed by the already-constructed value that assigns: count positivity from the triangulation-count bound lemma, mesh positivity from the admissible-family field, sinh domination from the Mathlib self-le-sinh characterization, and action comparison from the recognition-dominates-Regge lemma. No further tactics or case splits.
why it matters
Closes the existence side of the module's structural UV-finiteness theorem (status: 0 sorry, 0 RS-internal axiom). The module argument is that continuum EH non-renormalizability is an artifact of sending mesh to zero at fixed metric; the recognition substrate never takes that limit, and sinh suppression further damps large local curvature relative to Regge. This inhabited certificate is the Lean packaging of those three pillars (finite count, positive mesh cutoff, sinh domination).
No downstream consumers are recorded yet; the declaration sits at the end of the PathSumUVBound development as the inhabitance stamp on the certificate. Within the broader Recognition framework it supports the claim that gravity path sums remain UV-finite once the discrete substrate and recognition action replace continuum EH, consistent with the discrete geometric setting forced by the T0-T8 chain (eight-tick octave, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.