uv_cutoff_pos
plain-language theorem explainer
The RS ultraviolet cutoff on the cubic lattice is strictly positive. Gravity and continuum-limit arguments cite this to discharge the “cutoff exists” field of the cubic Regge convergence certificate. The proof unfolds the cutoff definition and finishes by Mathlib positivity.
Claim. The RS ultraviolet cutoff $\Lambda_{\mathrm{UV}}$ on the cubic lattice satisfies $0 < \Lambda_{\mathrm{UV}}$.
background
The module proves Regge convergence on the RS cubic lattice $\mathbb{Z}^3$ without the full Cheeger–Müller–Schrader regularity package. Four RS-specific structures replace CMS: perfect cube shape quality ($\sigma=1$), an eight-tick UV cutoff from the $2^3$ octave (T7), strict convexity of the $J$-cost, and the $\varphi$-exponential growth bound $\varphi^N > C\cdot N^3$.
The eight-tick periodicity supplies a natural mesh-scale cutoff: the lattice spacing is fixed by the fundamental voxel length $\ell_0$, so UV modes cannot run away. Spatial dimension is the forced $D=3$ of T8. The sibling definition uv_cutoff packages that positive scale; this theorem only records positivity.
Downstream, the cubic convergence certificate bundles positivity with shape quality, $\varphi$-growth, and the weak-field error estimate.
proof idea
Term-mode proof in two steps: unfold the definition of the UV cutoff, then apply Mathlib’s positivity tactic. No intermediate lemmas are needed; the expression is built from positive RS constants (powers of $\varphi$, fixed voxel scale), so the tactic closes immediately.
why it matters
Feeds the field uv_cutoff_exists of cubic_convergence_cert, the module’s packaged certificate that RS cubic Regge calculus converges. Without a strictly positive cutoff, the “no UV divergence from eight-tick periodicity” clause in the module strategy is empty.
In the framework this is the local positivity witness for T7’s eight-tick octave as a hard UV floor on $\mathbb{Z}^3$, paired with T8’s $D=3$ and the GrowthBounds $\varphi^N$ control on curvature concentration. It is a small but required discharge step so the certificate can claim unconditional $O(a^2)$ weak-field convergence without importing CMS aspect-ratio hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.