arctan_two_eq
plain-language theorem explainer
The identity arctan(2) equals pi over 4 plus arctan of 1/3 is obtained by splitting via the tangent addition formula after setting arctan(1) to pi/4. Numerics code that builds interval bounds for arctan cites this decomposition to reduce the argument to a known multiple of pi plus a smaller term. The tactic proof invokes Mathlib's arctan_add after checking the product condition, then closes with linear arithmetic.
Claim. $arctan 2 = pi/4 + arctan(1/3)$
background
The module supplies constructive interval bounds for arctan and tan via derivative comparisons. Upstream Interval structures from Numerics.Interval.Basic and Recognition.Certification define closed intervals with endpoints satisfying lo ≤ hi. The module documentation states that the arctan(2) identity is proved using Real.arctan_add from Mathlib, alongside polynomial bounds justified by monotoneOn_of_deriv_nonneg on [0, ∞).
proof idea
The tactic proof first rewrites arctan(1) to pi/4 using tan(pi/4) = 1 and arctan_tan. It then applies arctan_add to arctan(1) + arctan(1/3) after confirming the product is less than 1, normalizes, and finishes with linarith.
why it matters
This feeds arctan_two_in_interval, which rewrites the equality and applies add_contains_add to place arctan(2) inside arctanTwoInterval. It supplies the exact splitting identity required by the trig module's constructive bounds, supporting the numerics layer that underpins Recognition Science interval computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.