rk4Increment
rk4Increment encodes the classical fourth-order Runge-Kutta weighted sum that advances an ODE solution by step size h. Physicists discretizing the renormalization group flow for fermion mass residues cite it when approximating the integrated anomalous dimension. The definition is a direct algebraic expression with no lemmas or tactics.
claimFor step size $h$ and stage derivatives $k_1,k_2,k_3,k_4$, the increment is given by $h(k_1 + 2k_2 + 2k_3 + k_4)/6$.
background
The RGTransport module supplies the integral framework for the mass residue $f$ that appears in the Recognition Science mass formula, where physical masses relate to structural masses at the anchor scale via powers of the golden ratio. The residue is obtained by integrating the mass anomalous dimension over logarithmic scale. Numerical integration of the underlying ODE employs classical Runge-Kutta methods, for which this increment provides the update rule. The module imports cellular automaton stepping to model discrete dynamics and self-reference structures to certify meta-realization properties.
proof idea
The declaration is a direct one-line definition implementing the classical RK4 formula without invoking any lemmas or tactics.
why it matters in Recognition Science
This definition is the arithmetic kernel for rk4Step and the associated error bounds abs_rk4Increment_le and rk4Step_deviation_le. It supports numerical computation of the RG transport that defines the empirical mass residue, linking the continuous flow to the phi-ladder mass formula in the framework. The module notes that full QCD kernels remain external.
scope and limits
- Does not define the anomalous dimension function itself.
- Does not prove convergence or stability of the integrator.
- Does not connect directly to the phi-ladder or forcing chain.
Lean usage
def rk4Step (f : ℝ → ℝ) (x h : ℝ) : ℝ := let k1 := f x; let k2 := f (x + (h / 2) * k1); let k3 := f (x + (h / 2) * k2); let k4 := f (x + h * k3); x + rk4Increment h k1 k2 k3 k4formal statement (Lean)
149def rk4Increment (h k1 k2 k3 k4 : ℝ) : ℝ :=
proof body
Definition body.
150 (h / 6) * (k1 + 2 * k2 + 2 * k3 + k4)
151
152/-- One RK4 step for `x' = f(x)` with step size `h`. -/