BID coefficient correctness and complete datum round trips

BID coefficient and exponent packing satisfies the field bounds and recovers every valid datum after encoding. Every decoded word is valid; canonicalization preserves the complete datum and is idempotent.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.encodeFinite_lt (f : Format) (c e : ℕ) (hc : c < f.coefficientBound) (he : e < f.exponentBound) : encodeFinite f c e < 30 * (f.exponentBase * f.trailingBase)

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decodeFinite_valid (f : Format) (n : ℕ) (hn : n < 30 * (f.exponentBase * f.trailingBase)) : (decodeFinite f n).1 < f.coefficientBound ∧ (decodeFinite f n).2 < f.exponentBound

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decodeFinite_encodeFinite (f : Format) (c e : ℕ) (hc : c < f.coefficientBound) (he : e < f.exponentBound) : decodeFinite f (encodeFinite f c e) = (c, e)

Recover both the coefficient and the biased exponent from either steering branch.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decodeFinite_oversized (f : Format) (n : ℕ) (h : f.coefficientBound ≤ rawCoefficient f n) : decodeFinite f n = (0, biasedExponent f n)

Oversized BID significands denote zero while retaining the encoded exponent.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decodePayload_oversized (f : Format) (n : ℕ) (h : f.payloadBound ≤ n) : decodePayload f n = 0

An excessive BID NaN payload denotes zero rather than a decimal remainder.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.lawful : codec.Lawful

The executable BID fields satisfy the shared codec laws.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decode_encode (f : Format) (d : Datum) (h : Datum.Valid f d) : decode f (codec.encode f d) = d

Encoding and decoding preserve a representable datum exactly.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decode_valid (f : Format) (word : BitVec f.bitWidth) : Datum.Valid f (decode f word)

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.decode_canonicalize (f : Format) (word : BitVec f.bitWidth) : decode f (canonicalize f word) = decode f word

Canonicalizing a BID word preserves its sign, quantum exponent, and special metadata.

theorem FloatLib.Floats.Formats.DecimalInterchange.BID.canonicalize_idempotent (f : Format) (word : BitVec f.bitWidth) : canonicalize f (canonicalize f word) = canonicalize f word