Real semantics of two-coordinate arctangent comparisons

Both prepared and uncached comparators agree with the principal complex argument for every rational pair and rational boundary. The argument at (0, 0) is zero, and the Posit invalid-input policy belongs to the format wrapper. In units of π, quadrant and diagonal points compare equal to their rational values.

theorem FloatLib.Numerics.TrigonometricComparison.prepareAtan2_eq_real (x y : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareAtan2 x y levels).compare boundary = cmp { re := ↑x, im := ↑y }.arg ↑boundary

Prepared radian comparisons agree with the principal complex argument.

theorem FloatLib.Numerics.TrigonometricComparison.compareAtan2_eq_real (x y boundary : ℚ) : compareAtan2 x y boundary = cmp { re := ↑x, im := ↑y }.arg ↑boundary

Radian comparisons agree with the principal argument for every rational input.

theorem FloatLib.Numerics.TrigonometricComparison.prepareAtan2_neg_one_eq_real (levels : ℕ) (boundary : ℚ) : (prepareAtan2 (-1) 0 levels).compare boundary = cmp Real.pi ↑boundary

At (-1, 0) the prepared comparator compares π, the argument of -1, and shares its enclosures across boundaries.

theorem FloatLib.Numerics.TrigonometricComparison.prepareAtan2Pi_eq_real (x y : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareAtan2Pi x y levels).compare boundary = cmp ({ re := ↑x, im := ↑y }.arg / Real.pi) ↑boundary

Prepared pi-scaled comparisons agree with the argument divided by π, equality cases included.

theorem FloatLib.Numerics.TrigonometricComparison.compareAtan2Pi_eq_real (x y boundary : ℚ) : compareAtan2Pi x y boundary = cmp ({ re := ↑x, im := ↑y }.arg / Real.pi) ↑boundary

Pi-scaled comparisons agree with the principal argument divided by π.