Internal lemmas for directed rational packing

The rational packing proofs share three IEEE facts: subnormal fields are finite, the smallest normal field pair is finite, and positive upward overflow produces positive infinity.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Packing.Internal.isFinite_ofFields_subnormal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (mantissa : ℕ) (_hmantissa : mantissa < 2 ^ fmt.fracWidth) : (ofFields fmt false 0 mantissa).isFinite = true

An in-range IEEE subnormal fraction field denotes a finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Packing.Internal.isFinite_ofFields_minNormal (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : (ofFields fmt false 1 0).isFinite = true

The canonical IEEE minimum-normal field pair denotes a finite value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Packing.Internal.directedOverflow_false_true_eq_posInf (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : directedOverflow fmt false true = posInf fmt

Positive IEEE overflow rounds to positive infinity when the direction is upward.