optimal_h
plain-language theorem explainer
The definition supplies the step size h that minimizes the composite error bound δ(h) = ε/h² + (1+B) K h /3 arising in quantitative stability analysis for near-solutions of the d'Alembert equation. Researchers studying stability of functional equations or transfer of bounds from the cost functional to hyperbolic functions would cite the resulting O(ε^{1/3}) rate. The expression is obtained by setting the derivative of δ with respect to h to zero and extracting the positive real root of the resulting cubic.
Claim. Let ε, B, K > 0. The minimizing step size is given by $h = (6ε/((1+B)K))^{1/3}$.
background
The d'Alembert module studies quantitative closeness of C³ even functions H with H(0)=1 to the hyperbolic cosine when the defect Δ_H(t,u) = H(t+u) + H(t-u) - 2 H(t) H(u) is small. The composite error δ(h) balances the contribution of the defect bound ε scaled by 1/h² against the third-derivative remainder scaled by h, with B the uniform bound on |H| and K the uniform bound on |H'''|.
proof idea
The definition is the explicit positive root obtained by setting dδ/dh = 0, which produces the cubic equation h³ = 6ε/((1+B)K).
why it matters
The definition supplies the concrete h that realizes the O(ε^{1/3}) error rate inside the main stability estimate (Theorem 7.1) and its corollary transferring bounds to the cost functional F. It therefore supports the quantitative passage from small defect in the shifted cost H = J + 1 to proximity with cosh, consistent with the J-uniqueness step (T5) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.