Exact meanings of P3109 value queries

The executable predicates are connected to the exact decoder rather than to an approximate host conversion. The statements apply to every valid descriptor, including precision one.

theorem FloatLib.Floats.ExecFloat.P3109.decode_eq_decodeNat {format : Formats.P3109.Format} (value : P3109 format) : value.decode = format.decodeNat value.toNatBits

The raw natural-number decoder and the public decoder have the same exact observation.

theorem FloatLib.Floats.ExecFloat.P3109.isFinite_iff_decode {format : Formats.P3109.Format} (value : P3109 format) : value.isFinite = true ↔ ∃ (exact : Numerics.Dyadic), value.decode = Numerics.NumericalValue.finite exact

The finite query is true precisely when exact decoding produces a finite dyadic.

theorem FloatLib.Floats.ExecFloat.P3109.isInfinite_iff_decode {format : Formats.P3109.Format} (value : P3109 format) : value.isInfinite = true ↔ ∃ (negative : Bool), value.decode = Numerics.NumericalValue.infinity negative

The infinity query is true precisely when exact decoding produces either signed infinity.

theorem FloatLib.Floats.ExecFloat.P3109.isOne_iff_toClosedRat {format : Formats.P3109.Format} (value : P3109 format) : value.isOne = true ↔ value.toClosedRat = Numerics.NumericalValue.finite 1

Testing for one agrees with equality of the exact rational observation to one.

theorem FloatLib.Floats.ExecFloat.P3109.abs_toRat_of_decode_finite {format : Formats.P3109.Format} (value : P3109 format) (exact : Numerics.Dyadic) (hdecode : value.decode = Numerics.NumericalValue.finite exact) : |exact.toRat| = (format.decodePositiveFinite value.magnitudeBits).toRat

Removing the sign partition gives the exact absolute value of every finite datum.

theorem FloatLib.Floats.ExecFloat.P3109.isNormal_iff_decode {format : Formats.P3109.Format} (value : P3109 format) : value.isNormal = true ↔ ∃ (exact : Numerics.Dyadic), value.decode = Numerics.NumericalValue.finite exact ∧ (format.decodePositiveFinite (2 ^ format.trailingBits)).toRat ≤ |exact.toRat|

Normality is an exact absolute-value bound at the first normal magnitude code.

theorem FloatLib.Floats.ExecFloat.P3109.isSubnormal_iff_decode {format : Formats.P3109.Format} (value : P3109 format) : value.isSubnormal = true ↔ ∃ (exact : Numerics.Dyadic), value.decode = Numerics.NumericalValue.finite exact ∧ 0 < |exact.toRat| ∧ |exact.toRat| < (format.decodePositiveFinite (2 ^ format.trailingBits)).toRat

Subnormality is an exact nonzero absolute-value bound below the first normal value.

theorem FloatLib.Floats.ExecFloat.P3109.isZero_iff_toClosedRat {format : Formats.P3109.Format} (value : P3109 format) : value.isZero = true ↔ value.toClosedRat = Numerics.NumericalValue.finite 0

The unique zero code is precisely the datum with exact rational observation zero.

theorem FloatLib.Floats.ExecFloat.P3109.isSignMinus_iff_less_zero {format : Formats.P3109.Format} (value : P3109 format) : value.isSignMinus = true ↔ value.less zero = true

The sign query is precisely strict numerical comparison with zero; NaN is unordered.