Exact comparisons for two-coordinate arctangent

The input order is (x, y), giving the principal argument of x + i*y in (-π, π]. C and MPFR write atan2 (y, x), so a wrapper in that convention swaps the coordinates once, before preparing the comparator. The point (-1, 0) has argument π, which makes prepareAtan2 (-1) 0 an exact π comparator. Ordinary comparisons share reduced arctangent and π enclosures across rounding boundaries. Comparisons in units of π use the exact rational quadrant shift and the pi-scaled arctangent comparator, including its rational special values.

Both comparators use zero as the value at the origin, matching Mathlib's totalized argument. Posit wrappers must reject (0, 0) before rounding, as required by the Posit Standard.

Reference

• Posit Standard (2022), §5.5 and footnote 11, https://posithub.org/docs/posit_standard-2.pdf

def FloatLib.Numerics.TrigonometricComparison.prepareAtan2 (x y : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare comparisons of arg (x + i*y) with rational boundaries. The first levels enclosure depths are cached, and refinement past that prefix is unbounded.

def FloatLib.Numerics.TrigonometricComparison.compareAtan2 (x y boundary : ℚ) : Ordering

Compare the principal argument of x + i*y with a rational radian boundary.

def FloatLib.Numerics.TrigonometricComparison.prepareAtan2Pi (x y : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare comparisons of arg (x + i*y) / π, using an exact rational quadrant shift. No rounded approximation of π and no intermediate rounding enter the comparison.

def FloatLib.Numerics.TrigonometricComparison.compareAtan2Pi (x y boundary : ℚ) : Ordering

Compare the principal argument of x + i*y, divided by π, with a rational boundary.