inv_one_add_sq_le_upper
plain-language theorem explainer
The inequality states that the reciprocal of one plus t squared is bounded above by the quartic 1 minus t squared plus t to the fourth, for every real number t. Numerics code for trigonometric interval arithmetic cites this to establish the upper Taylor bound on arctan. The short proof multiplies through by the positive denominator, expands the left-hand product to one plus t to the sixth, and invokes non-negativity of a square to finish the comparison.
Claim. $1/(1 + t^2) ≤ 1 - t^2 + t^4$ for all real $t$.
background
This declaration lives in the Numerics.Interval.Trig module, which supplies rigorous interval bounds for arctan and tan via constructive derivative comparisons. The module proves that arctan(x) is bounded above by the partial sum x - x³/3 + x⁵/5 on the non-negative reals because the derivative comparison 1/(1+t²) ≤ 1 - t² + t⁴ holds; both sides integrate to the stated polynomials. The same module gives the matching lower bound using a similar sextic comparison.
proof idea
The tactic proof first rewrites the target inequality via div_le_iff₀, using positivity of the denominator. It then expands the product (1 - t² + t⁴)(1 + t²) by ring to obtain 1 + t⁶. Finally linarith closes the goal once the non-negativity of (t³)² is supplied, yielding 1 + t⁶ ≥ 1.
why it matters
This inequality is the key algebraic step that lets the module conclude arctan(x) ≤ g_upper(x) for x ≥ 0, where g_upper is the degree-five Taylor polynomial. The parent result arctan_le_upper_poly is then used wherever the Recognition Science numerics require tight upper bounds on arctan, for instance when computing the fine-structure constant interval (137.030, 137.039) or when calibrating the phi-ladder mass formula. It closes one of the constructive bounds needed for the eight-tick octave and D = 3 spatial dimension derivations in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.