Containment, convergence, and separation for the principal argument

The rational quadrant reduction gives both endpoint containment and convergence. Outside the nonnegative real axis, the argument cannot be rational: its tangent is the rational slope, whereas tangent at a nonzero rational angle is irrational. This proves that adaptive comparison terminates at every rational boundary, including the vertical and negative real axes.

theorem FloatLib.Numerics.TrigonometricComparison.contains_atan2Interval (x y : ℚ) (degree : ℕ) : (atan2Interval x y degree).Contains { re := ↑x, im := ↑y }.arg

The rational argument enclosure contains the exact principal value.

theorem FloatLib.Numerics.TrigonometricComparison.tendsto_atan2Interval_lo (x y : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(atan2Interval x y n).lo) Filter.atTop (nhds { re := ↑x, im := ↑y }.arg)

Lower rational argument endpoints converge to the exact principal value.

theorem FloatLib.Numerics.TrigonometricComparison.tendsto_atan2Interval_hi (x y : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(atan2Interval x y n).hi) Filter.atTop (nhds { re := ↑x, im := ↑y }.arg)

Upper rational argument endpoints converge to the exact principal value.

theorem FloatLib.Numerics.TrigonometricComparison.arg_ne_ratCast (x y boundary : ℚ) (hnonzero : ¬(0 ≤ x ∧ y = 0)) : { re := ↑x, im := ↑y }.arg ≠ ↑boundary

A rational complex point outside the nonnegative real axis has no rational argument.

theorem FloatLib.Numerics.TrigonometricComparison.exists_atan2_separating (x y boundary : ℚ) (hnonzero : ¬(0 ≤ x ∧ y = 0)) : ∃ (n : ℕ), Enclosure.Comparison.Separates (atan2Interval x y (2 ^ n)) boundary

Refinement eventually separates every rational boundary away from the exact zero branch.