Correct rounding from exact algebraic comparisons

The certificate bridge proves nearest-even rounding for every interior target. Monotonicity and the even tie at half the least subnormal cover the complete underflow interval. A finite IEEE result excludes the explicit overflow branch. Thus the real theorem needs no search-budget or distance-from-boundaries premise, and includes exact ties and subnormal results.

The real-refinement theorem uses a conventional IEEE descriptor, matching the existing logical rounding bridge. Runtime handling of custom descriptors is separate from this theorem.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.roundAt_halfMinSubnormal (fmt : FloatFormat) : roundAt fmt (Flocq.bpow Numerics.binaryRadix (lowerExponent fmt)) = 0

The midpoint between zero and the least subnormal rounds to the even endpoint, zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.roundAt_eq_zero_of_le_halfMinSubnormal (fmt : FloatFormat) (target : ℝ) (hnonneg : 0 ≤ target) (hsmall : target ≤ Flocq.bpow Numerics.binaryRadix (lowerExponent fmt)) : roundAt fmt target = 0

Every nonnegative target at or below the first midpoint rounds to zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.toReal_round_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (compare : ℚ → Ordering) (target : ℝ) (hnonneg : 0 ≤ target) (hcompare : ∀ (candidate : ℚ), compare candidate = cmp target ↑candidate) (hfinite : (round fmt sign compare).isFinite = true) : (round fmt sign compare).toReal = roundAt fmt (if sign = true then -target else target)

An exact oracle produces one nearest-even rounding of its signed real target.

The sole numerical-domain premise is nonnegativity of the magnitude. Finiteness of the packed IEEE result excludes overflow; underflow to signed zero and all midpoint ties are covered.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.toReal_root_eq_roundAt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (radicand : ℚ) (degree : ℕ) (target : ℝ) (hnonneg : 0 ≤ target) (hdegree : degree ≠ 0) (hroot : target ^ degree = ↑radicand) (hfinite : (root fmt sign radicand degree).isFinite = true) : (root fmt sign radicand degree).toReal = roundAt fmt (if sign = true then -target else target)

Exact integer-power comparisons correctly round any characterized nonnegative root.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.toReal_root_eq_roundAt_rpow (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (radicand : ℚ) (degree : ℕ) (hrad : 0 ≤ radicand) (hdegree : degree ≠ 0) (hfinite : (root fmt sign radicand degree).isFinite = true) : (root fmt sign radicand degree).toReal = roundAt fmt (if sign = true then -↑radicand ^ (↑degree)⁻¹ else ↑radicand ^ (↑degree)⁻¹)

The nonnegative real root exists for every nonnegative radicand and positive degree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AlgebraicRounding.toReal_root_two_eq_roundAt_sqrt (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (sign : Bool) (radicand : ℚ) (hrad : 0 ≤ radicand) (hfinite : (root fmt sign radicand 2).isFinite = true) : (root fmt sign radicand 2).toReal = roundAt fmt (if sign = true then -√↑radicand else √↑radicand)

Degree two rounds the exact square root, including zero.