Correctness of comparator-based posit rounding

A comparator agreeing with real order makes exactly the same decisions as the real rounding specification. No assumption about irrationality, distance from a boundary, or search convergence is needed: exact equality is one of the comparator's three results.

theorem FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.lowerCode_eq_real (format : Format) (compareTarget : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (q : ℚ), compareTarget q = cmp target ↑q) : lowerCode format compareTarget = RealRounding.lowerCode format target

An exact comparator selects the same lower code as real rounding.

theorem FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.roundCode_eq_real (format : Format) (compareTarget : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (q : ℚ), compareTarget q = cmp target ↑q) : roundCode format compareTarget = RealRounding.roundPositiveCode format target

Exact rational comparisons suffice for the complete positive real rounding rule.

theorem FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.round_eq_real (format : Format) (compareTarget : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (q : ℚ), compareTarget q = cmp target ↑q) : round format compareTarget = RealRounding.roundPositive format target

The executable model is the result selected by the real posit specification.

theorem FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.compare_neg_eq_real (compareTarget : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (q : ℚ), compareTarget q = cmp target ↑q) (q : ℚ) : (compareTarget (-q)).swap = cmp (-target) ↑q

Reversing comparisons with negated candidates compares the negated target.

theorem FloatLib.Floats.Formats.Posit.Model.ComparisonRounding.roundSigned_eq_real (format : Format) (compareTarget : ℚ → Ordering) (target : ℝ) (hcompare : ∀ (q : ℚ), compareTarget q = cmp target ↑q) : roundSigned format compareTarget = RealRounding.round format target

Exact target comparisons also suffice for the complete signed real rounding rule.