uv_cutoff
plain-language theorem explainer
The ultraviolet cutoff wavenumber on the RS cubic lattice is fixed at π/4, read off from the eight-tick period. Anyone proving Regge or lattice-field convergence in this module cites it as the built-in UV scale that replaces CMS regularity. The declaration is a bare real constant, not a derived bound.
Claim. The ultraviolet cutoff wavenumber is $\pi/4$.
background
The module develops Regge convergence on the RS cubic lattice $\mathbb{Z}^3$ without the full Cheeger–Müller–Schrader (CMS) package. Four structural facts replace CMS: perfect cube shape quality ($\sigma=1$), an eight-tick UV cutoff, strict convexity of the $J$-cost, and a $\varphi$-exponential growth bound.
The eight-tick octave (forcing step T7) supplies a natural highest resolvable wavenumber once the mesh is locked to the fundamental voxel length $\ell_0$. In lattice units that scale is written $\pi/4$. Downstream certificates record positivity of this cutoff alongside shape quality and $\varphi>1$ as the three RS-specific advantages.
The only named dependency is a positivity primitive from the rational-field layer; it is not used in the body of the constant itself, only in the positivity lemma that follows.
proof idea
Pure definition: the real constant is assigned the value $\operatorname{Real.pi}/4$. No tactics, no lemmas. The companion theorem uv_cutoff_pos unfolds the definition and closes positivity by the standard positivity tactic.
why it matters
Feeds the RS-specific convergence certificate CubicConvergenceCert, whose field uv_cutoff_exists requires $0 < \texttt{uv_cutoff}$, and the positivity lemma that discharges that field. The module strategy treats the eight-tick UV cutoff as the reason UV divergences never appear on the cubic lattice, so mesh size $a=\ell_0$ stays fixed and weak-field $O(a^2)$ convergence is unconditional. Landmark link: T7 (eight-tick octave, period $2^3$). Without a concrete positive cutoff the certificate cannot record the second structural advantage of the RS lattice over generic CMS triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.