Exact comparisons for two-coordinate arctangent

The input order is (x, y), giving the principal argument of x + i*y in (-π, π]. 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; refinement beyond that prefix remains 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 to π and no intermediate rounding enters 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.