Range safety for P3109 encoding

The direct encoder receives a rounded dyadic rather than searching a finite codebook. This module proves that an in-range value on the descriptor's precision grid produces an in-range code and decodes to the same numerical datum. The argument is uniform in bit width, precision, signedness, and finite or extended domain.

theorem FloatLib.Floats.Formats.P3109.Format.maxFiniteBits_lt_modulus (format : Format) : format.maxFiniteBits < format.modulus

The largest finite positive code is always inside the descriptor width.

theorem FloatLib.Floats.Formats.P3109.Format.maxFiniteBits_pos (format : Format) : 0 < format.maxFiniteBits

Every valid P3109 descriptor has a nonzero positive finite endpoint.

theorem FloatLib.Floats.Formats.P3109.Format.maxFiniteBits_lt_signBoundary_of_signed (format : Format) (signed : format.signedness = Signedness.signed) : format.maxFiniteBits < format.signBoundary

Positive finite codes stay below the sign boundary of a signed descriptor.

theorem FloatLib.Floats.Formats.P3109.Format.encodePositiveFinite_le_maxFiniteBits (format : Format) (value : Numerics.Dyadic) (hnegative : value.negative = false) (hzero : value.significand ≠ 0) (hprecision : value.significand ≤ 2 ^ format.precision) (hexponent : format.minimumQuantumExponent ≤ value.exponent) (hmax : value.toRat ≤ format.maxFinite.toRat) : Internal.encodePositiveFinite format value ≤ format.maxFiniteBits

Encoding a positive grid value no larger than maxFinite cannot overflow into a reserved code.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_fitsPrecisionGrid (format : Format) (bits : ℕ) : format.FitsPrecisionGrid (format.decodePositiveFinite bits)

Every decoded positive finite row lies on the descriptor precision grid.

theorem FloatLib.Floats.Formats.P3109.Format.maxFinite_fitsPrecisionGrid (format : Format) : format.FitsPrecisionGrid format.maxFinite

The positive finite endpoint lies on the descriptor precision grid.

theorem FloatLib.Floats.Formats.P3109.Format.maxFinite_toRat_pos (format : Format) : 0 < format.maxFinite.toRat

The positive finite endpoint is strictly positive.

theorem FloatLib.Floats.Formats.P3109.Format.minFinite_toRat_le_maxFinite (format : Format) : format.minFinite.toRat ≤ format.maxFinite.toRat

The descriptor's finite interval is nonempty.

theorem FloatLib.Floats.Formats.P3109.Format.minFinite_fitsPrecisionGrid (format : Format) : format.FitsPrecisionGrid format.minFinite

The negative or zero finite endpoint lies on the descriptor precision grid.

theorem FloatLib.Floats.Formats.P3109.Format.sameDatum_decode_encodeFinite (format : Format) (value : Numerics.Dyadic) (hgrid : format.FitsPrecisionGrid value) (hmin : format.minFinite.toRat ≤ value.toRat) (hmax : value.toRat ≤ format.maxFinite.toRat) : SameDatum (format.decode (BitVec.ofNat format.bitWidth (Internal.encodeDatumNat format (Numerics.NumericalValue.finite value)))) (Numerics.NumericalValue.finite value)

Direct encoding preserves every finite datum on the descriptor grid and inside its finite range.

This theorem is the no-wrap boundary used by projection correctness. It applies to arbitrary valid descriptors rather than a list of named low-precision formats.