h_lower_deriv
plain-language theorem explainer
The derivative of the lower arctan bounding polynomial equals 1 minus t squared plus t to the fourth minus t to the sixth at every real t. Researchers constructing rigorous bounds on arctan for numerical evaluations of constants cite this to confirm the derivative comparison step. The proof is a term-mode assembly of hasDerivAt combinators for the identity and odd-power terms followed by ring normalization.
Claim. Let $h(t) := t - t^3/3 + t^5/5 - t^7/7$. Then $h$ is differentiable at every real $t$ with derivative $1 - t^2 + t^4 - t^6$.
background
This declaration belongs to the module on interval arithmetic for trigonometric functions, which supplies constructive bounds on arctan via derivative comparison. The function h_lower is the truncated series $t - t^3/3 + t^5/5 - t^7/7$, whose derivative is the target polynomial; the module documentation states that the inequality $1 - t^2 + t^4 - t^6 ≤ 1/(1 + t^2)$ follows from the algebraic identity $(1 - t^2 + t^4 - t^6)(1 + t^2) = 1 - t^8 ≤ 1$ and is used with monotoneOn_of_deriv_nonneg on the nonnegative reals. Upstream results include the definition of h_lower in the same module together with basic interval subtraction from Numerics.Interval.Basic.
proof idea
The proof is a term-mode calculation. It unfolds the definition of h_lower, assembles the derivative from hasDerivAt_id, hasDerivAt_pow (for powers 3, 5, 7) with div_const, combines the terms by addition and subtraction, and converts the result to the target polynomial via ring.
why it matters
This derivative statement feeds the downstream theorem lower_poly_le_arctan, which asserts that the polynomial lies below arctan(x) for x ≥ 0. It supplies the explicit derivative needed for the monotoneOn_of_deriv_nonneg argument that closes the lower bound in the module's constructive strategy. In the Recognition Science setting the resulting arctan bounds support exact numerical work on constants such as π and the fine-structure constant within the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.