rk4Step_deviation_le
plain-language theorem explainer
The theorem bounds the displacement after one classical fourth-order Runge-Kutta step by |h| times the uniform bound M on the right-hand side at the four stage points. Analysts integrating renormalization-group flow equations for fermion mass residues would cite the result to control local truncation error when the anomalous dimension is supplied numerically. The proof unfolds the step definition, transfers the four pointwise bounds via simpa, invokes the companion increment lemma, and finishes with ring simplification.
Claim. Let $f:ℝ→ℝ$ and $x,h,M∈ℝ$. Assume $|f(x)|≤M$, $|f(x+(h/2)f(x))|≤M$, $|f(x+(h/2)f(x+(h/2)f(x)))|≤M$, and $|f(x+h⋅f(x+(h/2)f(x+(h/2)f(x))))|≤M$. Then the absolute deviation of the RK4 update from the initial value satisfies $|RK4(f,x,h)-x|≤|h|M$.
background
The module supplies the mathematical framework for renormalization-group transport of mass residues. The integrated residue is given by $f(μ₀,μ₁)=(1/λ)∫_{ln μ₀}^{ln μ₁} γ_m(μ') d(ln μ')$ with λ=ln ϕ; the physical mass then relates to the structural mass at the anchor scale by the factor ϕ^{-f}. The present theorem is a numerical-analysis auxiliary that controls one-step displacement when the right-hand side (anomalous dimension or beta function) is bounded by M at the RK4 nodes. Upstream results include the scale definition scale(k)=ϕ^k and structural theorems on primitive distinctions and simplicial ledgers, but the immediate dependency is the increment bound in the same file.
proof idea
The tactic proof unfolds rk4Step, names the four stage values k1 to k4, transfers the supplied bounds to these values with simpa, applies abs_rk4Increment_le to obtain the increment bound, records that the deviation equals the increment by ring_nf, and concludes by simpa.
why it matters
The result supplies a concrete error-control lemma inside the RG transport module that implements the residue factor appearing in the Recognition Science mass formula. It supports numerical evaluation of the integrated anomalous dimension that converts structural masses on the phi-ladder into physical masses. No downstream theorem yet consumes it; the declaration therefore closes a supporting gap in the numerical layer of the mass-residue computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.