rs_integral_finite
plain-language theorem explainer
The theorem shows that the RS-regulated integral stays bounded for any positive lower limit m below the ultraviolet cutoff p_max. QFT researchers modeling loop corrections with discrete spacetime would cite the result to justify finite predictions without ad-hoc cutoffs. The proof supplies the explicit majorant Real.log(p_max / m) + 1 and discharges the inequality by linear arithmetic after unfolding the integral definition.
Claim. For every real number $m > 0$ with $m < p_{max}$, there exists a real number $B$ such that the RS-regulated integral from $m$ to $p_{max}$ is strictly less than $B$.
background
The QFT.UVCutoff module derives a natural ultraviolet cutoff from Recognition Science discreteness at the fundamental scale τ₀, with p_max defined as ℏ/τ₀. This cutoff restricts momentum integrals and removes the ultraviolet divergences that appear in conventional QFT loop calculations. The regulatedIntegral function encodes the finite range from a positive mass threshold m to this p_max.
proof idea
The proof is a one-line term-mode construction that exhibits the bound Real.log(p_max / m) + 1. It unfolds the definition of regulatedIntegral and applies the linarith tactic to confirm the inequality under the supplied hypotheses m > 0 and p_max > m.
why it matters
The result supplies the finiteness step required for the running-coupling analysis that follows the φ-ladder in the same module. It directly implements the module claim that spacetime discreteness at τ₀ yields first-principles regularization of QFT divergences. The theorem sits upstream of the Brillouin-zone and lattice-cutoff statements that close the ultraviolet regularization argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.