abs_rk4Increment_le
plain-language theorem explainer
The algebraic bound shows that the RK4 increment (h/6)(k1 + 2k2 + 2k3 + k4) satisfies |increment| ≤ |h| M whenever each stage value ki obeys |ki| ≤ M. Numerical analysts integrating renormalization-group flows for mass anomalous dimensions would cite the enclosure to control local truncation error. The proof expands the weighted sum via three applications of the triangle inequality, scales the coefficients with nlinarith, and finishes by direct rewriting and gcongr.
Claim. If $|k_1| ≤ M$, $|k_2| ≤ M$, $|k_3| ≤ M$ and $|k_4| ≤ M$, then $|(h/6)(k_1 + 2k_2 + 2k_3 + k_4)| ≤ |h| M$.
background
The module supplies the mathematical framework for renormalization-group transport of mass residues, expressing the integrated anomalous dimension residue f(μ₀, μ₁) that relates structural mass at the anchor scale to physical mass via m_phys = m_struct · φ^{-f}. The RK4 increment is the standard fourth-order step (h/6)(k1 + 2k2 + 2k3 + k4) used to advance numerical integration of the beta or gamma functions. Upstream results include the definition of rk4Increment together with add_assoc and the norm_add_le triangle inequality from the arithmetic foundation.
proof idea
The tactic proof applies norm_add_le three times to obtain |k1 + 2k2 + 2k3 + k4| ≤ |k1| + 2|k2| + 2|k3| + |k4|, using abs_mul to handle the factors of 2. It then invokes nlinarith on the four stage bounds to reach a sum ≤ 6M. The final calc block rewrites the increment via abs_mul and abs_div, applies gcongr to the scaled product, and simplifies the arithmetic with ring.
why it matters
The bound is invoked directly by rk4Step_deviation_le to control the one-step deviation of the numerical transport map. It therefore supplies the local error estimate required for the RGTransport module that defines the empirical mass residue f^exp. Within Recognition Science the result supports controlled integration along the phi-ladder, ensuring that the mass formula yardstick · φ^(rung-8+gap(Z)) remains numerically stable when anomalous dimensions are evaluated at successive scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.