Order of positive finite IEEE P3109 codes

Positive finite codes are ordered by their unsigned natural-number representation. This module proves that the exact decoder preserves that order for every valid descriptor, including the subnormal-to-normal boundary and the P = 1 case.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_strictMono (format : Format) : StrictMono fun (bits : ℕ) => (format.decodePositiveFinite bits).toRat

Increasing a positive finite P3109 code strictly increases its exact numerical value.

The theorem is parameterized by the descriptor; no named width, precision, or format profile is enumerated.