Finite-value correctness for P3109 projection

Positive-row encoding and decoding preserve the rational value of a positive dyadic on the descriptor's precision grid, including the carry significand 2^P. These formulas use natural numbers without an upper exponent bound. Projection.Range adds the finite-range and bit-width bounds needed for full datum encoding.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_encodeRow_toRat (format : Format) (shifted : ℕ) (encodedExponent : ℤ) (hlt : shifted < 2 * 2 ^ format.trailingBits) (hmin : format.minimumNormalExponent ≤ encodedExponent) (hsubnormal : shifted < 2 ^ format.trailingBits → encodedExponent = format.minimumNormalExponent) : (format.decodePositiveFinite (if shifted < 2 ^ format.trailingBits then shifted % 2 ^ format.trailingBits else shifted % 2 ^ format.trailingBits + (encodedExponent + Int.ofNat format.exponentBias).toNat * 2 ^ format.trailingBits)).toRat = ↑shifted * 2 ^ (encodedExponent - Int.ofNat format.trailingBits)

Decoding the code that the encoder assembles from a row-scaled significand.

shifted is the significand scaled into the selected exponent row, so it is below 2^P, and it is below 2^(P-1) only when that row is the subnormal one.

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

Positive-row encoding preserves every positive dyadic accepted by the precision grid.

The significand bound is not strict: the carry value 2^P, produced when precision rounding increments an all-ones significand, is encoded in the next exponent row. The exponent lower bound is the smallest P3109 quantum, so the theorem covers every normal and subnormal row of every valid descriptor.