p_max
plain-language theorem explainer
Definition of the fundamental momentum cutoff as the ratio of the reduced Planck constant to the fundamental length scale. Researchers deriving natural UV regularizers for QFT loop integrals from spacetime discreteness cite this quantity. The construction is a direct assignment from the imported constants ħ and ℓ₀.
Claim. $p_max := ħ / ℓ₀$, where ℓ₀ denotes the fundamental length scale ℓ₀ = c τ₀.
background
The QFT.UVCutoff module derives the ultraviolet cutoff from Recognition Science discreteness at the τ₀ scale. Spacetime discreteness implies that field momenta cannot exceed a maximum value set by the ratio of ħ to the fundamental length, thereby regularizing all UV divergences in loop integrals. The module states that this supplies a first-principles regularization without external renormalization procedures.
proof idea
The declaration is a direct one-line definition that divides the reduced Planck constant by the fundamental length scale. It applies the upstream definitions of ħ (both native and CODATA forms) and ℓ₀ = c τ₀ without invoking additional lemmas or tactics.
why it matters
This supplies the momentum scale referenced by the Brillouin cutoff equality, the theorem that the RS cutoff exceeds LHC energies by seven orders of magnitude, and the finiteness result for regulated integrals. It realizes the core claim of QFT-013 that discreteness at τ₀ yields natural UV regularization, linking to the phi-ladder and eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.