arctan_one_third_in_interval
The result shows that arctan(1/3) lies inside the rational interval [0.321, 0.322]. Researchers building machine-checked enclosures for inverse trigonometric functions cite this when assembling rigorous bounds for π and related constants. The proof splits the containment into lower and upper parts, invokes derivative-comparison lemmas to replace arctan by explicit polynomials, substitutes the polynomial values at 1/3, and discharges the resulting rational inequalities by normalization and linear arithmetic.
claim$321/1000 ≤ arctan(1/3) ≤ 322/1000$
background
This declaration sits in the Numerics.Interval.Trig module, which supplies constructive interval arithmetic for arctan via polynomial bounds obtained from derivative comparisons. The target interval is the closed rational interval [321/1000, 322/1000]. The upper bounding polynomial is x − x³/3 + x⁵/5; the lower bound uses the degree-7 polynomial x − x³/3 + x⁵/5 − x⁷/7. Both comparisons rest on the fact that the difference between each polynomial and arctan is monotone on [0, ∞) because its derivative is nonnegative.
proof idea
The tactic proof splits the containment into two goals. The lower goal applies the general lower-polynomial inequality at x = 1/3, substitutes the explicit rational value of the lower polynomial, casts everything to reals, and finishes with linarith. The upper goal applies the general upper-polynomial inequality at x = 1/3, substitutes the explicit value of the upper polynomial, and again closes with linarith after normalization.
why it matters in Recognition Science
The enclosure is required by the downstream theorem establishing an interval for arctan(2) via the addition formula arctan(2) = π/4 + arctan(1/3). Within the Recognition Science framework these bounds support the constructive computation of π that enters the eight-tick octave and the derivation of the fine-structure constant interval (137.030, 137.039). It closes a concrete numerical step in the numerics layer that underpins later mass-to-light derivations.
scope and limits
- Does not compute a decimal expansion of arctan(1/3) beyond the stated interval.
- Does not prove the enclosure for any argument other than 1/3.
- Does not address convergence rates of the bounding polynomials.
- Does not extend the bounds to negative arguments or complex values.
formal statement (Lean)
130theorem arctan_one_third_in_interval :
131 arctanOneThirdInterval.contains (arctan (1 / 3)) := by
proof body
Tactic-mode proof.
132 simp only [contains, arctanOneThirdInterval]
133 constructor
134 · -- lower: ↑(321/1000 : ℚ) ≤ arctan(1/3)
135 have hlo := lower_poly_le_arctan (1 / 3) (by norm_num)
136 have hval : h_lower (1 / 3) = 24628 / 76545 := by unfold h_lower; norm_num
137 rw [hval] at hlo
138 have hq : ((321 / 1000 : ℚ) : ℝ) ≤ (24628 : ℝ) / 76545 := by push_cast; norm_num
139 linarith
140 · -- upper: arctan(1/3) ≤ ↑(322/1000 : ℚ)
141 have hhi := arctan_le_upper_poly (1 / 3) (by norm_num)
142 have hval : g_upper (1 / 3) = 391 / 1215 := by unfold g_upper; norm_num
143 rw [hval] at hhi
144 have hq : (391 : ℝ) / 1215 ≤ ((322 / 1000 : ℚ) : ℝ) := by push_cast; norm_num
145 linarith
146
147/-! ## §3. Constructive arctan(2) interval via addition formula -/
148
149/-- **PROVED**: `arctan(2) = π/4 + arctan(1/3)`.
150 From the addition formula: `arctan(1) + arctan(1/3) = arctan(2)`. -/