rk4Increment
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.