Value, range, and error of rational projection

The precision rounder can produce at most one carry. Carry normalization and preferred-cohort selection preserve its exact value. Every result, including a directed overflow result, is representable in its destination format.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_zero (f : Format) (mode : RoundingMode) (s : Bool) : roundedPair f mode s 0 = (0, f.minQuantum)

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_eq (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (preferred : ℤ) : projectMagnitude f mode s x preferred = have result := roundedPair f mode s x; if f.maxQuantum < result.2 then { value := if mode.overflowToInfinity s = true then Datum.infinity s else f.maxFinite s, status := { overflow := true, inexact := true } } else have inexact := decide (↑result.1 * 10 ^ result.2 ≠ x); { value := if inexact = true then Datum.finite s result.1 result.2 else preferredCohort f s result.1 result.2 preferred, status := { underflow := decide (x < f.minNormal) && inexact, inexact := inexact } }

Direct zero delivery agrees with precision rounding, cohort selection and all flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundAt_le_coefficientBound (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : mode.roundAt s x (roundingQuantum f x) ≤ f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_coefficient_lt (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : (roundedPair f mode s x).1 < f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_quantum_ge_min (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) : f.minQuantum ≤ (roundedPair f mode s x).2

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_value (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) : ↑(roundedPair f mode s x).1 * 10 ^ (roundedPair f mode s x).2 = ↑(mode.roundAt s x (roundingQuantum f x)) * 10 ^ roundingQuantum f x

Carry normalization preserves the computed value exactly.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.maxFinite_valid (f : Format) (s : Bool) : Datum.Valid f (f.maxFinite s)

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_valid (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) : Datum.Valid f (projectMagnitude f mode s x preferred).value

Every rational projection produces a valid datum, including underflow and overflow.

theorem FloatLib.Floats.Formats.DecimalInterchange.project_valid (f : Format) (mode : RoundingMode) (x : ℚ) (preferred : ℤ) (negativeZero : Bool) : Datum.Valid f (project f mode x preferred negativeZero).value

The signed public entry point is valid for every rational input.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_value (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (preferred : ℤ) (hq : (roundedPair f mode s x).2 ≤ f.maxQuantum) : (projectMagnitude f mode s x preferred).value.toRat? = some ((if s = true then -1 else 1) * ↑(mode.roundAt s x (roundingQuantum f x)) * 10 ^ roundingQuantum f x)

On the finite path, the datum denotes exactly the rounded coefficient-grid value.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hq : (roundedPair f mode s x).2 ≤ f.maxQuantum) : ∃ (value : ℚ), (projectMagnitude f mode s x preferred).value.toRat? = some value ∧ |value - if s = true then -x else x| ≤ 10 ^ roundingQuantum f x / 2

The finite result has at most half a decimal grid unit of error in either nearest mode.