pith. sign in
module module high

IndisputableMonolith.QFT.UVCutoff

show as:
view Lean formalization →

The UVCutoff module contrasts the ultraviolet divergence of standard QFT loop integrals with a physical cutoff enforced by Recognition Science discreteness. QFT researchers deriving regularization from first principles would cite it when replacing artificial Lambda with the RS lattice scale. The module is a definition collection that imports the time quantum and phi-forcing to introduce cutoff objects.

claimThe integral $I = ∫ d^4k / (k^2 - m^2)^n$ diverges for $n ≤ 2$ as $k → ∞$; RS supplies a physical cutoff from lattice discreteness rather than an artificial $Λ → ∞$.

background

The module opens with the standard QFT UV problem for loop integrals of the form $I = ∫ d^4k / (k^2 - m^2)^n$. It imports the RS time quantum $τ_0 = 1$ tick from Constants and the self-similarity argument from PhiForcing, whose doc states: 'This module proves that φ is forced by self-similarity in a discrete ledger with J-cost.' The local setting is therefore a discrete ledger whose J-cost structure forces the golden ratio and thereby a finite spatial cutoff.

proof idea

This is a definition module, no proofs. It defines standardUVDescription, log_divergence, l0, E0, p_max, rsCutoffGeV and related objects that encode the contrast between artificial and physical cutoffs.

why it matters in Recognition Science

The module supplies the UV cutoff foundation for the parent QFT module, whose doc states it contains 'Tier 2 Derivations (from MASTER_DERIVATION_LIST_TIER2.md)'. It thereby links the physical cutoff directly to the phi-forced discrete ledger of the forcing chain.

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)