arctan_two_in_interval
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.