lower_poly_le_arctan
plain-language theorem explainer
The inequality x − x³/3 + x⁵/5 − x⁷/7 ≤ arctan(x) holds for every real x ≥ 0. Numerics developers constructing rigorous enclosures for arctan(1/3) cite the result to anchor their lower estimate. The argument reduces the claim to nonnegativity of the difference function, establishes its monotonicity on [0, ∞) by verifying a nonnegative derivative via lower_le_inv_one_add_sq, and checks the zero value at the origin.
Claim. $x - x^3/3 + x^5/5 - x^7/7 ≤ arctan(x)$ for all real $x ≥ 0$.
background
The module supplies constructive interval bounds for arctan via derivative comparison. h_lower is the explicit polynomial x − x³/3 + x⁵/5 − x⁷/7 whose derivative equals 1 − t² + t⁴ − t⁶. Upstream results establish that h_lower is continuous and differentiable, together with the comparison lower_le_inv_one_add_sq that places this derivative below 1/(1 + t²). The local setting follows the module's use of monotoneOn_of_deriv_nonneg on the ray [0, ∞) to obtain all arctan bounds constructively.
proof idea
The proof reduces the target to nonnegativity of arctan x − h_lower x. It applies monotoneOn_of_deriv_nonneg on the convex set Ici 0 after confirming continuity of the difference and differentiability on the interior. The derivative comparison 1/(1 + t²) − (1 − t² + t⁴ − t⁶) ≥ 0 follows from lower_le_inv_one_add_sq. The difference vanishes at zero by direct evaluation, so monotonicity forces the inequality for all x ≥ 0.
why it matters
This theorem supplies the lower half of the arctan interval bounds required by arctan_one_third_in_interval, which establishes that arctan(1/3) lies inside a rational interval. That enclosure is used to obtain a rigorous value for arctan(2) = π/4 + arctan(1/3) and therefore for π itself. Within the Recognition Science framework the result closes the lower-bound step of the eight-tick octave numerics that ultimately constrains the fine-structure constant inside (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.