Mathematical order and extrema for P3109

Finite extrema agree with the rational field's minimum and maximum. Comparisons agree with rational order, while NaN stays unordered. Magnitude ties and the preference for finite values are stated apart from rounding. The executable extrema use the same binary refinement as arithmetic, so these identities describe the expression at their single projection boundary. Clamping rejects reversed bounds and agrees with the rational interval clamp for ordered bounds.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.less_finite (left right : ℚ) : less (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = true ↔ left < right

Finite strict comparison is rational strict order.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.lessEqual_finite (left right : ℚ) : lessEqual (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = true ↔ left ≤ right

Finite non-strict comparison is rational order.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.equal_finite (left right : ℚ) : equal (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = true ↔ left = right

Finite comparison equality is equality of rational values.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.less_self (value : Numerics.NumericalValue ℚ) : less value value = false

No datum is strictly less than itself, even NaN.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimum_finite (left right : ℚ) : minimum (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Numerics.NumericalValue.finite (min left right)

Finite minimum is the ordinary rational minimum.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximum_finite (left right : ℚ) : maximum (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Numerics.NumericalValue.finite (max left right)

Finite maximum is the ordinary rational maximum.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimum_comm (left right : Numerics.NumericalValue ℚ) : minimum left right = minimum right left

Exact closed minimum is commutative, including NaN and infinity.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximum_comm (left right : Numerics.NumericalValue ℚ) : maximum left right = maximum right left

Exact closed maximum is commutative, including NaN and infinity.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimumFinite_finite_infinity (value : ℚ) (negative : Bool) : minimumFinite (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.infinity negative) = Numerics.NumericalValue.finite value

A finite operand wins over either infinity in minimum-finite.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximumFinite_finite_infinity (value : ℚ) (negative : Bool) : maximumFinite (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.infinity negative) = Numerics.NumericalValue.finite value

A finite operand wins over either infinity in maximum-finite.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimumNumber_nan_finite (value : ℚ) : minimumNumber nan (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite value

The number variant ignores NaN in favor of a finite operand.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximumNumber_nan_finite (value : ℚ) : maximumNumber nan (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite value

The number variant ignores NaN in favor of a finite operand.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimumMagnitude_neg_self (value : ℚ) (hvalue : 0 ≤ value) : minimumMagnitude (Numerics.NumericalValue.finite (-value)) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite (-value)

Equal nonnegative magnitudes are resolved toward the negative datum by minimum.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximumMagnitude_neg_self (value : ℚ) (hvalue : 0 ≤ value) : maximumMagnitude (Numerics.NumericalValue.finite (-value)) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite value

Equal nonnegative magnitudes are resolved toward the positive datum by maximum.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.clamp_of_reversed (value lower upper : Numerics.NumericalValue ℚ) (hbounds : greater lower upper = true) : clamp value lower upper = nan

Reversed clamp bounds have the report's indeterminate NaN result.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.clamp_finite (value lower upper : ℚ) (hbounds : lower ≤ upper) : clamp (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.finite lower) (Numerics.NumericalValue.finite upper) = Numerics.NumericalValue.finite (min (max value lower) upper)

Clamping a finite value between ordered finite bounds gives the rational interval clamp.

theorem FloatLib.Floats.ExecFloat.P3109.decode_clamp {format : Formats.P3109.Format} (value lower upper : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (value.clamp lower upper target mode saturation).decode (target.projectRatValue { rounding := mode, saturation := saturation } (Formats.P3109.Arithmetic.clamp value.toClosedRat lower.toClosedRat upper.toClosedRat))

Clamp encoding refines the exact closed clamp followed by one report projection.