rk4Step
The fourth-order Runge-Kutta step computes a single update for the autonomous ODE x' = f(x) by evaluating four successive stages and applying the standard weighted increment. Physicists discretizing the integrated mass residue in RG flow would invoke it to advance the anomalous-dimension integral numerically. The definition is a direct transcription of the classical stages followed by the auxiliary increment formula.
claimThe fourth-order Runge-Kutta update for the autonomous equation $x' = f(x)$ with step size $h$ is given by $x + (h/6)(k_1 + 2k_2 + 2k_3 + k_4)$, where $k_1 = f(x)$, $k_2 = f(x + (h/2)k_1)$, $k_3 = f(x + (h/2)k_2)$, and $k_4 = f(x + h k_3)$.
background
This module supplies the mathematical framework for renormalization-group transport of mass residues. Fermion masses run according to $d(ln m)/d(ln μ) = -γ_m(μ)$, and the integrated residue $f(μ_0, μ_1) = (1/λ) ∫ γ_m d(ln μ)$ with λ = ln φ converts structural masses on the phi-ladder to physical masses via $m_phys = m_struct · φ^{-f}$. The RK4 step is introduced to integrate such transport equations numerically when explicit kernels are unavailable. It depends on the auxiliary definition that supplies the weighted average (h/6)(k1 + 2k2 + 2k3 + k4).
proof idea
The definition evaluates the four classical stages k1 = f(x), k2 = f(x + (h/2)k1), k3 = f(x + (h/2)k2), k4 = f(x + h k3) and returns x plus the increment supplied by the auxiliary weighted-average definition. It is a direct transcription of the standard algorithm with no additional lemmas or tactics.
why it matters in Recognition Science
This definition supplies the numerical integrator required to discretize the RG transport that defines the empirical mass residue. It is invoked by the one-step deviation bound that encloses |rk4Step f x h - x| ≤ |h| M and by the fixed-point identity that recovers x when the forcing vanishes. In the Recognition Science setting it enables concrete evaluation of the integrated residue that appears in the structural-to-physical mass conversion on the phi-ladder.
scope and limits
- Does not prove global convergence or truncation-error bounds for the integrator.
- Does not extend to non-autonomous, time-dependent, or vector-valued ODEs.
- Does not incorporate adaptive step-size selection or error control.
- Does not embed the explicit QCD or QED anomalous-dimension kernels.
formal statement (Lean)
153def rk4Step (f : ℝ → ℝ) (x h : ℝ) : ℝ :=
proof body
Definition body.
154 let k1 := f x
155 let k2 := f (x + (h / 2) * k1)
156 let k3 := f (x + (h / 2) * k2)
157 let k4 := f (x + h * k3)
158 x + rk4Increment h k1 k2 k3 k4
159