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

isFinite is true iff 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

isInfinite is true iff exact decoding produces a 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 zero code is the only datum whose exact rational observation is zero.

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

isSignMinus agrees with strict comparison against zero, under which NaN is unordered.