Decimal coefficient bounds

Projection, square root and adjacent-value proofs use the same relation between a full coefficient and its trailing digits. These consequences of the descriptor laws apply to every admissible custom layout as well as the named presets.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.payloadBound_eq (f : Format) : f.payloadBound = 10 ^ (f.precision - 1)

The trailing digits fill all but one position of the significand precision.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.payloadBound_lt_coefficientBound (f : Format) : f.payloadBound < f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.payloadBound_le_coefficientBound_sub_one (f : Format) : f.payloadBound ≤ f.coefficientBound - 1

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.one_lt_coefficientBound (f : Format) : 1 < f.coefficientBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.carry_eq (f : Format) (coefficient : ℕ) (quantum : ℤ) : Numerics.RadixText.carry 10 ⟨f.precision, ⋯⟩ coefficient quantum = if coefficient = f.coefficientBound then (f.payloadBound, quantum + 1) else (coefficient, quantum)

A carry at the coefficient bound leaves exactly one leading digit. This identifies the generic radix carry with the descriptor's coefficient limits.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.carry_coefficient_lt (f : Format) {coefficient : ℕ} (hc : coefficient ≤ f.coefficientBound) (quantum : ℤ) : (Numerics.RadixText.carry 10 ⟨f.precision, ⋯⟩ coefficient quantum).1 < f.coefficientBound

Normalizing a coefficient bounded by 10^precision makes the bound strict.

theorem FloatLib.Floats.Formats.DecimalInterchange.Format.le_carry_quantum (f : Format) (coefficient : ℕ) (quantum : ℤ) : quantum ≤ (Numerics.RadixText.carry 10 ⟨f.precision, ⋯⟩ coefficient quantum).2

A carry either preserves the quantum or increases it by one.