Range preservation before P3109 saturation

An input in the finite interval cannot round past either endpoint in any mode. The endpoint is an integer multiple of the input quantum, and each mode preserves integers and chooses one of the two adjacent candidates. Thus precision-rounding overflow implies that the exact input was already outside the finite interval. This is a one-way implication.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.roundedInteger_le_natCast (mode : RoundingMode) (negative : Bool) (parity : ℕ → Bool) (value : ℚ) (bound : ℕ) (hnonneg : 0 ≤ value) (hv : value ≤ ↑bound) : roundedInteger mode negative parity value ≤ bound

Choosing either adjacent candidate, while preserving integers, cannot cross an integer bound.

theorem FloatLib.Floats.Formats.P3109.RationalRounding.abs_roundAt_le_grid (mode : RoundingMode) (quantum : ℤ) (parity : ℕ → Bool) (value : ℚ) (significand : ℕ) (exponent : ℤ) (hq : quantum ≤ exponent) (hv : |value| ≤ ↑significand * 2 ^ exponent) : |roundAt mode quantum parity value| ≤ ↑significand * 2 ^ exponent

Rounding preserves an upper grid endpoint whenever the input quantum divides that endpoint.

theorem FloatLib.Floats.Formats.P3109.Format.decodePositiveFinite_significand_lt_precision (format : Format) (bits : ℕ) : (format.decodePositiveFinite bits).significand < 2 ^ format.precision

Decoding uses a strictly bounded significand; a carry is introduced only by rounding.

theorem FloatLib.Floats.Formats.P3109.Format.rationalQuantum_le_grid_exponent (format : Format) (value : ℚ) (significand : ℕ) (exponent : ℤ) (hvalue : value ≠ 0) (hs : significand < 2 ^ format.precision) (he : format.minimumQuantumExponent ≤ exponent) (hv : |value| ≤ ↑significand * 2 ^ exponent) : RationalRounding.quantum format.precision format.exponentBias value ≤ exponent

An in-range nonzero magnitude chooses a quantum dividing every upper grid bound.

theorem FloatLib.Floats.Formats.P3109.Format.abs_roundFiniteRatToPrecision_le_maxFinite (format : Format) (mode : RoundingMode) (value : ℚ) (hv : |value| ≤ format.maxFinite.toRat) : |(format.roundFiniteRatToPrecision mode value).toRat| ≤ format.maxFinite.toRat

Every mode preserves the finite magnitude bound before saturation.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_nonneg (format : Format) (mode : RoundingMode) (value : ℚ) (hv : 0 ≤ value) : 0 ≤ (format.roundFiniteRatToPrecision mode value).toRat

Rounding a nonnegative rational cannot introduce a negative result.

theorem FloatLib.Floats.Formats.P3109.Format.roundFiniteRatToPrecision_mem_range (format : Format) (mode : RoundingMode) (value : ℚ) (hlo : format.minFinite.toRat ≤ value) (hhi : value ≤ format.maxFinite.toRat) : format.minFinite.toRat ≤ (format.roundFiniteRatToPrecision mode value).toRat ∧ (format.roundFiniteRatToPrecision mode value).toRat ≤ format.maxFinite.toRat

The descriptor's closed finite interval is preserved by every supplied rounding mode.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.roundedExceedsFiniteRange_implies_outside (format : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (exact : ℚ) (hoverflow : roundedExceedsFiniteRange format mode exact = true) : exact < format.minFinite.toRat ∨ format.maxFinite.toRat < exact

Precision-rounding overflow entails that the exact rational was outside the finite interval. This holds before saturation, for every mode and every supplied stochastic word.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.roundedExceedsFiniteRange_implies_exceedsFiniteRange (format : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (exact : ℚ) (hoverflow : roundedExceedsFiniteRange format mode exact = true) : exceedsFiniteRange format exact = true

The executable overflow indicator implies the executable exact-out-of-range indicator.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.status_overflow_implies_outside (format : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (exact : ℚ) (hoverflow : (status format policy (Numerics.NumericalValue.finite exact)).overflow = true) : exact < format.minFinite.toRat ∨ format.maxFinite.toRat < exact

A finite conversion's overflow flag witnesses exclusion of its exact input from the range.