P3109 classification and adjacency facts

Positive finite code order is exact numerical order. It identifies the least positive value, the normal/subnormal boundary, and the absence of a representable value between consecutive magnitude codes. These facts apply to arbitrary valid descriptors, including precision one. The imported classification facet connects all eight value queries to exact decoding and order. The neighbor facet proves immediate adjacency and the absence of a neighbor at either endpoint, including infinite endpoints. The additional facts here expose the positive magnitude boundary and partition finite values into normal and subnormal cases.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_toRat_pos_iff (format : Format) (bits : ℕ) : 0 < (format.decodePositiveFinite bits).toRat ↔ 0 < bits

A positive magnitude code denotes a strictly positive rational, and code zero denotes zero.

theorem FloatLib.Floats.Formats.P3109.Format.minPositive_le_decodePositiveFinite (format : Format) (bits : ℕ) (hbits : 0 < bits) : (format.decodePositiveFinite 1).toRat ≤ (format.decodePositiveFinite bits).toRat

Code one is no larger than any strictly positive finite magnitude code.

theorem FloatLib.Floats.Formats.P3109.Format.minNormal_le_decodePositiveFinite_iff (format : Format) (bits : ℕ) : (format.decodePositiveFinite (2 ^ format.trailingBits)).toRat ≤ (format.decodePositiveFinite bits).toRat ↔ 2 ^ format.trailingBits ≤ bits

Normal magnitude codes denote precisely values at or above the first normal value.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_subnormal_iff (format : Format) (bits : ℕ) : 0 < (format.decodePositiveFinite bits).toRat ∧ (format.decodePositiveFinite bits).toRat < (format.decodePositiveFinite (2 ^ format.trailingBits)).toRat ↔ 0 < bits ∧ bits < 2 ^ format.trailingBits

Subnormal positive codes denote precisely nonzero values below the first normal value.

theorem FloatLib.Floats.Formats.P3109.Format.no_decodePositiveFinite_between (format : Format) (bits candidate : ℕ) : ¬((format.decodePositiveFinite bits).toRat < (format.decodePositiveFinite candidate).toRat ∧ (format.decodePositiveFinite candidate).toRat < (format.decodePositiveFinite (bits + 1)).toRat)

No finite positive magnitude code lies numerically between consecutive codes.

theorem FloatLib.Floats.Formats.P3109.Format.no_subnormal_of_precision_eq_one (format : Format) (hprecision : format.precision = 1) (bits : ℕ) : ¬(0 < bits ∧ bits < 2 ^ format.trailingBits)

Precision one leaves no strictly positive subnormal magnitude code.

theorem FloatLib.Floats.Formats.P3109.Format.maxSubnormalOf_eq_nan (format : Format) (hprecision : format.precision = 1) : format.maxSubnormalOf = ExecFloat.P3109.nan

The maximum-subnormal query returns the single NaN at precision one.

theorem FloatLib.Floats.ExecFloat.P3109.isFinite_of_isNormal {format : Formats.P3109.Format} (value : P3109 format) (h : value.isNormal = true) : value.isFinite = true

A normal value is finite.

theorem FloatLib.Floats.ExecFloat.P3109.isFinite_of_isSubnormal {format : Formats.P3109.Format} (value : P3109 format) (h : value.isSubnormal = true) : value.isFinite = true

A subnormal value is finite.

theorem FloatLib.Floats.ExecFloat.P3109.not_isNormal_and_isSubnormal {format : Formats.P3109.Format} (value : P3109 format) : ¬(value.isNormal = true ∧ value.isSubnormal = true)

Normal and subnormal classifications are disjoint.

theorem FloatLib.Floats.ExecFloat.P3109.isNormal_or_isSubnormal {format : Formats.P3109.Format} (value : P3109 format) (hfinite : value.isFinite = true) (hpositive : 0 < value.magnitudeBits) : value.isNormal = true ∨ value.isSubnormal = true

Every nonzero finite magnitude code is classified as either normal or subnormal.

theorem FloatLib.Floats.ExecFloat.P3109.isSubnormal_eq_false_of_precision_eq_one {format : Formats.P3109.Format} (value : P3109 format) (hprecision : format.precision = 1) : value.isSubnormal = false

Precision-one formats classify no value as subnormal.

theorem FloatLib.Floats.ExecFloat.P3109.nextGreaterThan_of_isNaN {format : Formats.P3109.Format} (value : P3109 format) (h : value.isNaN = true) : value.nextGreaterThan = nan

The upper neighbor of NaN is NaN.

theorem FloatLib.Floats.ExecFloat.P3109.nextLessThan_of_isNaN {format : Formats.P3109.Format} (value : P3109 format) (h : value.isNaN = true) : value.nextLessThan = nan

The lower neighbor of NaN is NaN.

theorem FloatLib.Floats.ExecFloat.P3109.nextGreaterThan_of_nonnegative {format : Formats.P3109.Format} (value : P3109 format) (hnan : value.isNaN = false) (hsign : value.isSignMinus = false) (hend : value.toNatBits ≠ format.positiveInfinityBits) : value.nextGreaterThan = ofNatBits (value.toNatBits + 1)

Interior nonnegative codes advance by one under the upper-neighbor operation.

theorem FloatLib.Floats.ExecFloat.P3109.nextLessThan_of_positive {format : Formats.P3109.Format} (value : P3109 format) (hnan : value.isNaN = false) (hzero : value.isZero = false) (hsign : value.isSignMinus = false) : value.nextLessThan = ofNatBits (value.toNatBits - 1)

Positive codes descend by one under the lower-neighbor operation.