The DPD combination field and exponent continuation

The DPD combination field packs a leading digit below 10 and a high exponent below 3, and its accessors recover both. Bounded exponent continuation and trailing fields pack below the combinations reserved for infinity and NaN.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.combination_lt (leading high : ℕ) (hl : leading < 10) (hh : high < 3) : combination leading high < 30

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.leadingDigit_lt (field : ℕ) : leadingDigit field < 10

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.highExponent_lt (field : ℕ) (h : field < 30) : highExponent field < 3

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.leadingDigit_combination (leading high : ℕ) (hl : leading < 10) (hh : high < 3) : leadingDigit (combination leading high) = leading

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.highExponent_combination (leading high : ℕ) (hl : leading < 10) (hh : high < 3) : highExponent (combination leading high) = high

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeFields_lt (f : Format) (leading e trailing : ℕ) (hl : leading < 10) (he : e < f.exponentBound) (ht : trailing < f.trailingBase) : encodeFields f leading e trailing < 30 * (f.exponentBase * f.trailingBase)

Assembling the DPD fields never collides with an infinity or NaN combination.

theorem FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeFields_extract (f : Format) (leading e trailing : ℕ) (ht : trailing < f.trailingBase) : have n := encodeFields f leading e trailing; n / (f.exponentBase * f.trailingBase) = combination leading (e / f.exponentBase) ∧ n / f.trailingBase % f.exponentBase = e % f.exponentBase ∧ n % f.trailingBase = trailing

The three stored fields can be recovered independently.