Pith. sign in
module module high

IndisputableMonolith.QFT.UVCutoff

show as:
view Lean formalization →

This module assembles definitions for the physical ultraviolet cutoff in Recognition Science QFT, replacing artificial regulators with a discreteness scale from the phi-ladder. QFT practitioners deriving finite loop integrals from RS foundations would cite it when moving from standard regularization to the Brillouin-zone boundary. The module imports Constants and PhiForcing to express the cutoff in RS-native units without performing explicit integrals.

claimThe RS ultraviolet cutoff is the physical momentum scale $p_{\max}$ at the Brillouin zone edge of the fundamental lattice, with associated energy $E_0$ and length $l_0$ set by the discrete phi-ladder; standard loop integrals $I = \int d^4k/(k^2-m^2)^n$ remain finite for $n\le 2$ once $k$ is bounded by this scale.

background

The module sits in the QFT domain and imports the RS time quantum $\tau_0=1$ tick together with the self-similarity argument that forces $\phi$ as the fixed point of the J-cost ledger. Its DOC_COMMENT states that standard QFT loop integrals diverge as $k\to\infty$ for $n\le 2$ and are regularized by an artificial $\Lambda\to\infty$, whereas RS supplies a physical cutoff from lattice discreteness.

Sibling definitions include standardUVDescription, log_divergence, l0, E0, p_max, lhcEnergyGeV, rsCutoffGeV, cutoff_above_lhc, VoxelLattice, fundamentalLattice, brillouinCutoff and brillouin_equals_pmax. These translate the abstract cutoff into concrete RS scales and compare them with LHC energies.

proof idea

This is a definition module, no proofs. It organizes constants and predicates that express the cutoff scale, the logarithmic divergence form, and the relation between the Brillouin cutoff and p_max.

why it matters in Recognition Science

The module supplies the UV regularization mechanism required by the parent QFT module for its Tier 2 derivations of quantum field theory fundamentals from Recognition Science. It directly implements the physical-cutoff claim in the supplied DOC_COMMENT and thereby closes the gap between the discrete phi-ladder (from PhiForcing) and continuum QFT expressions.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (26)