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 mathematical convention at (0, 0) is zero; the Posit invalid-input policy belongs to the format wrapper. Exact pi-scaled quadrant and diagonal values are included in the comparison contract.

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 exact 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 use the exact principal branch, with no restriction on rational inputs.

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 preserve the exact quadrant shift and every equality case.

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 exact argument divided by π.