add_contains_add
plain-language theorem explainer
add_contains_add establishes that if real x lies in interval I and y in J then x+y lies in the sum interval I+J. Numerics code verifying bounds on phi powers or arctan cites it to chain addition steps in interval arithmetic. The proof is a direct constructor that splits containment into lo and hi goals, simplifies via add_lo and add_hi, then applies add_le_add to the respective bound pairs.
Claim. Let $I=[a,b]$ and $J=[c,d]$ be closed intervals with rational endpoints. If $a≤x≤b$ and $c≤y≤d$ for real $x,y$, then $a+c≤x+y≤b+d$.
background
The module supplies verified interval arithmetic that uses rational endpoints to bound real values of transcendental functions. Interval is the structure with fields lo, hi : ℚ and valid : lo ≤ hi; containment of a real x holds precisely when lo ≤ x ≤ hi. Addition of intervals is defined componentwise on the rational endpoints, with add_lo and add_hi extracting the resulting lower and upper bounds after casting to ℝ.
proof idea
The term proof opens with constructor to split the containment goal into separate lower-bound and upper-bound subgoals. Each subgoal simplifies the interval sum definition via simp only [add_lo, Rat.cast_add] (respectively add_hi), then closes with exact add_le_add applied to the corresponding projections of the hypotheses hx and hy.
why it matters
The result is invoked directly in phi_pow_142_in_interval and arctan_two_in_interval to propagate verified bounds on golden-ratio powers and inverse trigonometric values. It supplies the basic addition rule needed for the numerics layer that checks constants arising from the phi-ladder and J-cost minimization in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.