Posit and decimal conversion semantics

Decimal destinations inherit the shared projection's validity, error and directed enclosure guarantees. Posit destinations equal the standard signed real-rounding specification for every finite decimal input, including saturation and nonzero underflow. No intermediate binary format is involved.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_eq_project {fmt : Posit.Format} (f : Format) (mode : RoundingMode) (x : Posit.Model fmt) {a : ℚ} (hx : x.toRat? = some a) : fromPosit f mode x = project f mode a 0

A finite posit is converted by decimal projection of its exact rational value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_valid {fmt : Posit.Format} (f : Format) (mode : RoundingMode) (x : Posit.Model fmt) : Datum.Valid f (fromPosit f mode x).value

Every posit conversion produces a valid destination datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_zero_clamped (fmt : Posit.Format) (f : Format) (mode : RoundingMode) : fromPosit f mode (Posit.Model.zero fmt) = { value := Datum.finite false 0 (max f.minQuantum (min 0 f.maxQuantum)) }

Posit zero becomes positive decimal zero, with preferred quantum zero clamped to the destination quantum range.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_zero (fmt : Posit.Format) (f : Format) [f.HasQuantumZero] (mode : RoundingMode) : fromPosit f mode (Posit.Model.zero fmt) = { value := Datum.finite false 0 0 }

When quantum zero is available, posit zero converts to positive decimal zero there.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_nar (fmt : Posit.Format) (f : Format) (mode : RoundingMode) : fromPosit f mode (Posit.Model.nar fmt) = { value := Datum.nan false false 0 }

NaR becomes a quiet, zero-payload decimal NaN, with no IEEE exception raised.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_error_le_half {fmt : Posit.Format} (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Posit.Model fmt) {a : ℚ} (hx : x.toRat? = some a) (hfinite : (fromPosit f mode x).status.overflow = false) : ∃ (value : ℚ), (fromPosit f mode x).value.toRat? = some value ∧ |value - a| ≤ 10 ^ roundingQuantum f |a| / 2

A nonoverflowing nearest decimal conversion has at most half a grid unit of error.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_error_lt_one {fmt : Posit.Format} (f : Format) (mode : RoundingMode) (x : Posit.Model fmt) {a : ℚ} (hx : x.toRat? = some a) (hfinite : (fromPosit f mode x).status.overflow = false) : ∃ (value : ℚ), (fromPosit f mode x).value.toRat? = some value ∧ |value - a| < 10 ^ roundingQuantum f |a|

In any rounding direction a nonoverflowing conversion changes the value by less than one decimal grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.le_fromPosit_towardPositive {fmt : Posit.Format} (f : Format) (x : Posit.Model fmt) {a : ℚ} (hx : x.toRat? = some a) (hfinite : (fromPosit f RoundingMode.towardPositive x).status.overflow = false) : ∃ (value : ℚ), (fromPosit f RoundingMode.towardPositive x).value.toRat? = some value ∧ a ≤ value

Upward posit-to-decimal conversion encloses the exact posit value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_towardNegative_le {fmt : Posit.Format} (f : Format) (x : Posit.Model fmt) {a : ℚ} (hx : x.toRat? = some a) (hfinite : (fromPosit f RoundingMode.towardNegative x).status.overflow = false) : ∃ (value : ℚ), (fromPosit f RoundingMode.towardNegative x).value.toRat? = some value ∧ value ≤ a

Downward posit-to-decimal conversion encloses the exact posit value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_inexact_iff {fmt : Posit.Format} (f : Format) (mode : RoundingMode) (x : Posit.Model fmt) {a value : ℚ} (hx : x.toRat? = some a) (hfinite : (fromPosit f mode x).status.overflow = false) (hout : (fromPosit f mode x).value.toRat? = some value) : (fromPosit f mode x).status.inexact = true ↔ value ≠ a

Without overflow, inexact is exactly a changed rational value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromPosit_underflow_iff {fmt : Posit.Format} (f : Format) (mode : RoundingMode) (x : Posit.Model fmt) {a : ℚ} (hx : x.toRat? = some a) (hfinite : (fromPosit f mode x).status.overflow = false) : (fromPosit f mode x).status.underflow = true ↔ |a| < f.minNormal ∧ (fromPosit f mode x).status.inexact = true

Decimal underflow is precisely an inexact tiny input when overflow is absent.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toPosit_nan (fmt : Posit.Format) (s signaling : Bool) (p : ℕ) : toPosit fmt (Datum.nan s signaling p) = Posit.Model.nar fmt

Decimal NaNs, whether signaling or quiet, convert to NaR.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toPosit_infinity (fmt : Posit.Format) (s : Bool) : toPosit fmt (Datum.infinity s) = Posit.Model.nar fmt

Either signed decimal infinity converts to NaR.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toPosit_zero (fmt : Posit.Format) (s : Bool) (q : ℤ) : toPosit fmt (Datum.finite s 0 q) = Posit.Model.zero fmt

Both decimal zero signs and every zero cohort convert to the unique posit zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toPosit_eq_real (fmt : Posit.Format) (x : Datum) {a : ℚ} (hx : x.toRat? = some a) : toPosit fmt x = Posit.Model.RealRounding.round fmt ↑a

Every finite decimal datum has exact single-rounding posit semantics. This includes range saturation and the standard nonzero-underflow rule without additional hypotheses.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.toPosit_eq_of_toRat?_eq (fmt : Posit.Format) {x y : Datum} (h : x.toRat? = y.toRat?) : toPosit fmt x = toPosit fmt y

Changing a decimal cohort does not change its posit conversion.