rk4Step_eq_self_of_zero
When the forcing function is identically zero, the fourth-order Runge-Kutta step returns the input state unchanged. This identity is invoked inside the RG transport module to confirm that a vanishing anomalous dimension produces no mass residue. The proof reduces immediately by unfolding the RK4 definitions and substituting the zero hypothesis.
claimLet $f : {R} {to} {R}$ satisfy $f(y) = 0$ for every real $y$. Then for any real numbers $x$ and $h$, the fourth-order Runge-Kutta step satisfies $rk4Step(f, x, h) = x$.
background
The module supplies the mathematical framework for renormalization-group transport of mass residues. The integrated residue is defined as the integral of the mass anomalous dimension gamma_m from the anchor scale to the physical scale, normalized by lambda = ln phi. This residue enters the mass formula relating the structural mass at mu_star to the observed physical mass via a power of phi.
proof idea
The proof is a one-line wrapper that applies simplification to the definitions of rk4Step and rk4Increment together with the hypothesis that f is identically zero.
why it matters in Recognition Science
The identity verifies that the RK4 integrator for the RG flow is algebraically consistent with the zero-residue case required by the mass formula. It belongs to the RGTransport module that supplies the transport layer into which QCD and QED anomalous-dimension kernels are intended to plug. No downstream uses are recorded yet.
scope and limits
- Does not establish truncation error bounds for nonzero forcing functions.
- Does not address stability or convergence of repeated RK4 steps.
- Does not incorporate concrete QCD or QED anomalous-dimension kernels.
formal statement (Lean)
160theorem rk4Step_eq_self_of_zero (f : ℝ → ℝ)
161 (hzero : ∀ y, f y = 0) (x h : ℝ) :
162 rk4Step f x h = x := by
proof body
Term-mode proof.
163 simp [rk4Step, rk4Increment, hzero]
164
165/-- Algebraic enclosure: if each RK4 stage is bounded by `M`, then one-step
166deviation is bounded by `|h|*M`. -/