lower_le_inv_one_add_sq
plain-language theorem explainer
The inequality 1 - t² + t⁴ - t⁶ ≤ 1/(1 + t²) holds for every real t. Interval-arithmetic researchers establishing rigorous lower bounds on arctan would cite it to justify the integral comparison that yields the degree-7 polynomial bound. The proof multiplies through by the positive denominator, expands the left-hand side algebraically to 1 - t⁸, and concludes via non-negativity of t⁸.
Claim. $1 - t^{2} + t^{4} - t^{6} ≤ 1/(1 + t^{2})$ for all real $t$.
background
The module supplies constructive interval bounds for arctan and tan. Its central technique compares the derivative 1/(1 + t²) of arctan against polynomials on [0, ∞) and integrates the resulting monotonicity statement via monotoneOn_of_deriv_nonneg. The lower-bound case requires precisely that 1 - t² + t⁴ - t⁶ ≤ 1/(1 + t²), whose integral is the degree-7 polynomial x - x³/3 + x⁵/5 - x⁷/7. The module document states that this comparison follows because the product (1 - t² + t⁴ - t⁶)(1 + t²) equals 1 - t⁸, which is at most 1.
proof idea
The tactic proof first rewrites the target using le_div_iff₀ (justified by positivity of 1 + t²). It then introduces the algebraic identity (1 - t² + t⁴ - t⁶)(1 + t²) = 1 - t⁸ obtained by ring, rewrites the inequality to 1 - t⁸ ≤ 1, and finishes with linarith applied to the non-negativity of (t⁴)².
why it matters
The lemma is the key algebraic step feeding lower_poly_le_arctan, which asserts the degree-7 lower bound on arctan for nonnegative arguments. Within Recognition Science this supplies the constructive lower estimate needed for interval arithmetic on trigonometric functions, supporting precise numerical evaluation of constants such as the inverse fine-structure constant inside (137.030, 137.039) and the phi-ladder relations that determine mass scales. It closes one half of the derivative-comparison chain described in the module document.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.