IndisputableMonolith.Numerics.Interval.Trig
The Numerics.Interval.Trig module supplies verified polynomial upper and lower bounds for arctan using rational-endpoint interval arithmetic. Researchers verifying constants in the Recognition framework cite it for certified estimates on transcendental functions. It defines g_upper as the polynomial x - x^3/3 + x^5/5, establishes smoothness properties, and proves the bounding inequalities through derivative comparisons.
claimThe module defines the upper bounding polynomial $g(x) = x - x^3/3 + x^5/5$ for arctan on the unit interval, the lower bound $h(x)$, and the theorems $g'(x) - 1/(1+x^2) > 0$ together with arctan$(x) < g(x)$ (and the symmetric lower statements), all with explicit continuity and differentiability of the bounding functions.
background
The module extends verified interval arithmetic from IndisputableMonolith.Numerics.Interval.Basic, which bounds real functions by exact rational endpoints. It also draws on rigorous bounds for π from the PiBounds module. Core objects are the polynomials g_upper and h_lower that envelope arctan, together with their derivatives and continuity statements that enable mean-value arguments.
proof idea
The module first defines g_upper(x) = x - x^3/3 + x^5/5 and proves it continuous and differentiable with explicit derivative. It then shows inv_one_add_sq_le_upper by direct comparison of 1/(1+x^2) to g_upper', after which arctan_le_upper_poly follows by integration of the positive difference or a mean-value application. Parallel definitions and steps hold for h_lower and lower_poly_le_arctan.
why it matters in Recognition Science
This module supplies the arctan bounds required for high-precision numerical verification of constants such as alpha inverse inside (137.030, 137.039) inside the Recognition framework. It feeds the numerics pipeline that supports mass-ladder calculations and J-uniqueness checks, closing the gap between abstract interval tools and concrete transcendental estimates.
scope and limits
- Does not supply bounds for |x| > 1.
- Does not treat sine, cosine, or other trigonometric functions.
- Does not include floating-point or approximate implementations.
- Does not claim optimality of the chosen polynomial degree.
depends on (2)
declarations in this module (17)
-
def
g_upper -
theorem
g_upper_continuous -
theorem
g_upper_differentiable -
theorem
g_upper_deriv -
theorem
inv_one_add_sq_le_upper -
theorem
arctan_le_upper_poly -
def
h_lower -
theorem
h_lower_continuous -
theorem
h_lower_differentiable -
theorem
h_lower_deriv -
theorem
lower_le_inv_one_add_sq -
theorem
lower_poly_le_arctan -
def
arctanOneThirdInterval -
theorem
arctan_one_third_in_interval -
theorem
arctan_two_eq -
def
arctanTwoInterval -
theorem
arctan_two_in_interval