regulatedIntegral
plain-language theorem explainer
The regulatedIntegral definition supplies the closed-form logarithmic expression for a UV-regulated loop integral under the Recognition Science momentum cutoff. QFT researchers in the RS framework cite it to bound divergences once the discrete p_max replaces the continuum limit. The definition is a direct one-line assignment to the natural logarithm of the cutoff-to-mass ratio.
Claim. For mass parameter $m > 0$ and cutoff parameter $Λ > m$, the regulated loop integral is defined by $I(m, Λ) := log(Λ / m)$.
background
Module QFT.UVCutoff develops the ultraviolet regularization that follows from Recognition Science discreteness at the τ₀ scale. The core claim is that spacetime discreteness imposes a maximum momentum p_max = ℏ / τ₀, which replaces the divergent upper limit in loop integrals. The supplied DOC_COMMENT states that the four-dimensional integral ∫ d⁴k / (k² + m²)² behaves as ln(Λ / m) for large Λ and becomes finite once Λ is set to p_max.
proof idea
This is a direct definition that equates the regulated integral to Real.log (Λ / m). No lemmas or tactics are invoked; the body is the explicit closed-form expression for the leading logarithmic divergence.
why it matters
The definition supplies the explicit finite expression consumed by the downstream theorem rs_integral_finite, which proves the integral remains bounded for any finite cutoff. It realizes the QFT-013 target of natural UV regularization from information-theoretic discreteness and connects the discrete τ₀ scale to the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.