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