g_upper_deriv
The derivative of the upper bounding polynomial g_upper at any real t equals 1 - t² + t⁴. Interval-arithmetic proofs for arctan bounds cite this to justify monotonicity of the error function via the monotone derivative theorem on the nonnegative reals. The proof is a direct term-mode computation that unfolds the polynomial definition, assembles the derivative from power rules, and normalizes the result by ring.
claimLet $g(t) := t - t^3/3 + t^5/5$. Then $g$ is differentiable at every real $t$ with $g'(t) = 1 - t^2 + t^4$.
background
The Numerics.Interval.Trig module constructs rigorous interval bounds for arctan by comparing derivatives on [0, ∞). The function g_upper is the explicit antiderivative of the rational upper bound 1 - t² + t⁴; the comparison 1 - t² + t⁴ ≥ 1/(1 + t²) follows from the algebraic identity (1 - t² + t⁴)(1 + t²) = 1 + t⁶ ≥ 1. The module imports basic interval arithmetic (including subtraction) and relies on Mathlib results for arctan continuity, differentiability, and the mean-value theorem.
proof idea
The term proof unfolds the definition of g_upper, then builds the derivative expression by subtracting the scaled cubic power derivative from the identity derivative and adding the scaled quintic power derivative. A single convert tactic with ring normalization confirms that the assembled expression equals 1 - t² + t⁴.
why it matters in Recognition Science
This derivative statement is the key step that lets the downstream theorem arctan_le_upper_poly apply monotoneOn_of_deriv_nonneg to the error g_upper(x) - arctan(x). It therefore supplies the constructive upper bound arctan(x) ≤ x - x³/3 + x⁵/5 used throughout the module's trigonometric interval arithmetic, which supports numerical evaluations required by the Recognition Science phi-ladder and constant derivations.
scope and limits
- Does not prove the inequality g_upper(t) ≥ 1/(1 + t²).
- Does not treat the corresponding lower-bound polynomial.
- Does not extend the derivative claim to complex arguments.
- Does not supply an explicit error bound between g_upper and arctan.
formal statement (Lean)
47private theorem g_upper_deriv (t : ℝ) :
48 HasDerivAt g_upper (1 - t ^ 2 + t ^ 4) t := by
proof body
Term-mode proof.
49 unfold g_upper
50 have := ((hasDerivAt_id t).sub ((hasDerivAt_pow 3 t).div_const 3)).add
51 ((hasDerivAt_pow 5 t).div_const 5)
52 convert this using 1; ring
53
54/-- Key inequality: `1/(1+t²) ≤ 1 − t² + t⁴` for all t.
55 Proof: `(1−t²+t⁴)(1+t²) = 1+t⁶ ≥ 1`. -/