Numerical classification, cohorts and stored canonicality

Zero, normal, and subnormal classification agrees with exact rational magnitudes and is preserved within a cohort. For a fixed encoding and format, canonical words are equal exactly when they decode to the same complete datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.minNormal_pos (f : Format) : 0 < f.minNormal

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.finiteValue_abs (s : Bool) (c : ℕ) (q : ℤ) : |finiteValue s c q| = ↑c * 10 ^ q

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.finiteValue_eq_zero_iff (s : Bool) (c : ℕ) (q : ℤ) : finiteValue s c q = 0 ↔ c = 0

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.isZero_iff (d : Datum) : d.isZero = true ↔ d.toRat? = some 0

The zero predicate agrees with exact rational semantics, at every quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.isNormal_iff (f : Format) (d : Datum) : isNormal f d = true ↔ ∃ (x : ℚ), d.toRat? = some x ∧ f.minNormal ≤ |x|

Normality is a numerical threshold test, independent of sign and cohort.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.isSubnormal_iff (f : Format) (d : Datum) : isSubnormal f d = true ↔ ∃ (x : ℚ), d.toRat? = some x ∧ x ≠ 0 ∧ |x| < f.minNormal

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_isNormal (f : Format) {x y : Datum} (h : x.SameCohort y) : isNormal f x = isNormal f y

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_isSubnormal (f : Format) {x y : Datum} (h : x.SameCohort y) : isSubnormal f x = isSubnormal f y

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.finite_classification (f : Format) (s : Bool) (c : ℕ) (q : ℤ) : have d := finite s c q; (d.isZero || isNormal f d || isSubnormal f d) = true

The finite classes exhaust zero, normal and subnormal values.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.classify_zero_iff (f : Format) (d : Datum) : classify f d = Numerics.IEEEClass.negativeZero ∨ classify f d = Numerics.IEEEClass.positiveZero ↔ d.isZero = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.classify_normal_iff (f : Format) (d : Datum) : classify f d = Numerics.IEEEClass.negativeNormal ∨ classify f d = Numerics.IEEEClass.positiveNormal ↔ isNormal f d = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.classify_subnormal_iff (f : Format) (d : Datum) : classify f d = Numerics.IEEEClass.negativeSubnormal ∨ classify f d = Numerics.IEEEClass.positiveSubnormal ↔ isSubnormal f d = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.classify_signalingNaN_iff (f : Format) (d : Datum) : classify f d = Numerics.IEEEClass.signalingNaN ↔ d.isSignaling = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.classify_infinite_iff (f : Format) (d : Datum) : classify f d = Numerics.IEEEClass.negativeInfinity ∨ classify f d = Numerics.IEEEClass.positiveInfinity ↔ d.isInfinite = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.classify_nan_iff (f : Format) (d : Datum) : classify f d = Numerics.IEEEClass.signalingNaN ∨ classify f d = Numerics.IEEEClass.quietNaN ↔ d.isNaN = true

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameQuantum_self (x : Datum) : x.sameQuantum x = true

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameQuantum_comm (x y : Datum) : x.sameQuantum y = y.sameQuantum x

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameQuantum_trans {x y z : Datum} (hxy : x.sameQuantum y = true) (hyz : y.sameQuantum z = true) : x.sameQuantum z = true

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Encoding.isCanonical_canonicalize (encoding : Encoding) (f : Format) (w : BitVec f.bitWidth) : encoding.isCanonical f (encoding.canonicalize f w) = true

Re-encoding always produces a canonical word, including on redundant input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Encoding.eq_iff_decode_eq (encoding : Encoding) (f : Format) {x y : BitVec f.bitWidth} (hx : encoding.isCanonical f x = true) (hy : encoding.isCanonical f y = true) : x = y ↔ encoding.decode f x = encoding.decode f y

Two canonical encodings in the same encoding and format are equal precisely when they decode to the same complete datum.