h_lower_continuous
Continuity of the lower arctan bounding polynomial is recorded here. Researchers on rigorous interval bounds for trigonometric functions cite it to license derivative monotonicity arguments. The proof is a one-line wrapper that unfolds the explicit polynomial and invokes fun_prop.
claimThe function $h(x) := x - x^3/3 + x^5/5 - x^7/7$ is continuous on the reals.
background
The module supplies constructive interval bounds for arctan via derivative comparison on [0, ∞). The lower bounding polynomial is the explicit antiderivative of 1 - t² + t⁴ - t⁶, obtained by integrating the rational inequality 1 - t² + t⁴ - t⁶ ≤ 1/(1 + t²). The upstream definition supplies the closed-form expression that enters all subsequent monotonicity statements.
proof idea
One-line wrapper: unfold the definition of the polynomial, then apply the fun_prop tactic which automatically verifies continuity of rational expressions built from addition, multiplication and division by nonzero constants.
why it matters in Recognition Science
The result is invoked inside lower_poly_le_arctan to feed the continuousOn hypothesis of monotoneOn_of_deriv_nonneg, thereby closing the lower bound arctan(x) ≥ x - x³/3 + x⁵/5 - x⁷/7. It forms part of the constructive arctan infrastructure used for high-precision numerical evaluation of constants such as α^{-1} inside the Recognition Science pipeline.
scope and limits
- Does not establish differentiability of the polynomial.
- Does not extend the continuity claim to the complex domain.
- Does not prove the arctan inequality itself.
- Applies only on the real line; no uniformity statements are given.
formal statement (Lean)
83private theorem h_lower_continuous : Continuous h_lower := by unfold h_lower; fun_prop