rk4Step
plain-language theorem explainer
The fourth-order Runge-Kutta step definition supplies the classical integrator for the scalar autonomous ODE x' = f(x). It is invoked when numerically integrating the renormalization-group flow of mass anomalous dimensions to obtain the residue that enters the Recognition Science mass formula. The body evaluates the four classical stages sequentially and delegates the weighted increment to the companion definition that computes (h/6)(k1 + 2k2 + 2k3 + k4).
Claim. The fourth-order Runge-Kutta step for the autonomous scalar ODE $x' = f(x)$ at position $x$ with step size $h$ is $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
The RGTransport module formalizes renormalization-group transport of mass residues. Fermion masses run according to $d(ln m)/d(ln μ) = -γ_m(μ)$, and the integrated residue is the normalized integral $f(μ_0, μ_1) = (1/λ) ∫_{ln μ_0}^{ln μ_1} γ_m(μ') d(ln μ')$ with λ = ln φ. This residue converts the structural mass at the anchor scale into the physical mass via $m_phys = m_struct · φ^{-f}$. Numerical evaluation of the integral for scale-dependent γ_m requires an ODE solver; the present definition supplies the classical fourth-order Runge-Kutta step for the autonomous equation x' = f(x). The upstream weighted-increment definition assembles each completed step from the four stage values.
proof idea
The definition is a direct computational encoding of the classical RK4 stages. It binds k1 to f(x), k2 to f(x + (h/2)k1), k3 to f(x + (h/2)k2), k4 to f(x + h k3), then returns x plus the result of the upstream weighted-increment definition applied to h, k1, k2, k3, k4. No tactics appear; the body is a pure let-binding sequence.
why it matters
This definition supplies the numerical engine that the one-step deviation bound and the zero-function fixed-point identity rely upon. It enables concrete computation of the RG transport integral that converts structural masses at the anchor scale into physical masses on the phi-ladder. Within the Recognition Science framework the integrated residue appears directly in the mass formula yardstick · φ^(rung - 8 + gap(Z)), so accurate numerical transport is required to match empirical residues. It touches the open question of supplying higher-order QCD kernels for the anomalous dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.