arctan_two_in_interval
The result places arctan(2) inside a concrete interval built from scaled pi bounds plus an arctan(1/3) enclosure. Numerics workers verifying trigonometric constants inside the Recognition Science stack would cite it when tightening bounds on alpha or ladder masses. The proof reduces the claim by the arctan addition identity then applies interval addition and a sibling enclosure for arctan(1/3).
claim$arctan(2)$ lies in the sum of the one-fourth scaled pi interval and the arctan of one-third interval.
background
The module supplies constructive interval enclosures for arctan and tan. Upper and lower polynomial bounds follow from derivative comparison: the upper polynomial is the antiderivative of (1-t^2+t^4) which dominates 1/(1+t^2) on [0,infty), while the lower polynomial uses the complementary inequality. The key identity arctan(2) equals pi/4 plus arctan(1/3) is taken from Mathlib's arctan_add. Interval addition is supplied by the sibling theorem that the sum of two intervals contains the sum of any points inside them.
proof idea
The term proof rewrites the target via the arctan addition identity, unfolds the target interval definition, then invokes interval addition. The first subgoal scales the pi interval by the positive rational 1/4 using the smul containment lemma and simplifies the resulting bounds by ring. The second subgoal is discharged directly by the sibling enclosure for arctan(1/3).
why it matters in Recognition Science
The lemma supplies a verified numerical anchor for arctan(2) that supports downstream constant checks inside the Recognition Science numerics layer. It closes the constructive path for the eight-tick octave and phi-ladder evaluations that ultimately feed the alpha band (137.030,137.039) and mass formulas. No direct parent theorems are listed among the used-by edges, leaving the result as a self-contained building block for future interval-based verifications.
scope and limits
- Does not supply enclosures for arctan at arguments other than 2.
- Does not treat complex-valued arctan.
- Does not tighten the interval width beyond the given polynomial-plus-pi construction.
- Does not address floating-point rounding error outside the interval model.
formal statement (Lean)
166theorem arctan_two_in_interval :
167 arctanTwoInterval.contains (arctan 2) := by
proof body
Term-mode proof.
168 rw [arctan_two_eq]
169 unfold arctanTwoInterval
170 apply add_contains_add
171 · -- π/4 is in (1/4) · piInterval
172 have hpi := pi_in_piInterval
173 have := smulPos_contains_smul (q := 1 / 4) (by norm_num : (0 : ℚ) < 1 / 4) hpi
174 simp only [Rat.cast_div, Rat.cast_one, Rat.cast_ofNat] at this
175 convert this using 1
176 ring
177 · exact arctan_one_third_in_interval
178
179end IndisputableMonolith.Numerics