h_lower
plain-language theorem explainer
The polynomial h_lower supplies the explicit lower approximant for arctan on the nonnegative reals in constructive interval arithmetic. Numerical proofs in musical scales, photobiomodulation devices, and constant bounds cite it to close intervals on arctan(2) and derived quantities. It is introduced by direct truncation of the alternating series after the x^7 term.
Claim. Define the polynomial $h(x) := x - x^3/3 + x^5/5 - x^7/7$. This function satisfies $h(x) ≤ arctan(x)$ for all real $x ≥ 0$.
background
The module supplies rigorous interval bounds for arctan and tan via derivative-comparison monotonicity. The lower bound rests on the pointwise inequality 1 - t² + t⁴ - t⁶ ≤ 1/(1 + t²) for t ≥ 0, whose antiderivative is exactly h(x). The comparison is obtained from monotoneOn_of_deriv_nonneg applied on [0, ∞).
proof idea
The declaration is a direct definition of the truncated Taylor polynomial; no lemmas or tactics are invoked beyond the syntactic expansion of the powers and coefficients.
why it matters
It is the concrete lower approximant referenced by 28 downstream results, including fifth_quality (12-TET interval error < 0.003), lambda_PBM_approx (766 nm window), k_R_bounds (Boltzmann constant in (0.47, 0.49)), and w_t_nonneg_with. In the Recognition framework it closes the arctan(2) = π/4 + arctan(1/3) identity that pins the alpha band and phi-ladder numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.