Direct encoding for P3109 projection

The direct encoder and decoder satisfy the inverse laws needed by P3109 projection. Further contracts relate executable datum comparison to the mathematical SameDatum relation and specify the checked encoder. Precision rounding and saturation correctness live in later modules.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.encodeDatumNat_decode (format : Format) (code : BitVec format.bitWidth) : Internal.encodeDatumNat format (format.decode code) = code.toNat

The direct natural-number encoder is a left inverse of exact-width decoding.

theorem FloatLib.Floats.Formats.P3109.Format.datumEqual_eq_true_iff (left right : Numerics.NumericalValue Numerics.Dyadic) : datumEqual left right = true ↔ SameDatum left right

Executable datum equality holds exactly for the same mathematical P3109 datum.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Format.encode?_decode (format : Format) (code : BitVec format.bitWidth) : format.encode? (format.decode code) = some code

Checked encoding is a left inverse of P3109 decoding.

theorem FloatLib.Floats.Formats.P3109.Format.sameDatum_decode_of_encode?_eq_some (format : Format) (value : Numerics.NumericalValue Numerics.Dyadic) (code : BitVec format.bitWidth) (success : format.encode? value = some code) : SameDatum (format.decode code) value

A successful checked encoding decodes to the same P3109 datum as its input.

No rounding occurs in encode?; success is exactly the representability certificate.