Semantics of mixed and scaled P3109 arithmetic

These results identify the exact expression passed to the final destination projection. The source types, their storage representations, and the destination format are independent. Finite hypotheses expose ordinary rational expressions. Without them, the closed operation keeps the report's NaN and infinity rules.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.decode_convert {Source SourceExact : Type} [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (format : Format) (value : Source) (mode : RoundingMode) (saturation : SaturationMode) : Format.SameDatum (convert (Destination.p3109 format) value mode saturation).decode (format.projectRatValue { rounding := mode, saturation := saturation } (decode value))

Generic conversion to P3109 decodes to one report projection of the exact source datum.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.decode_unary {Source SourceExact : Type} [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (format : Format) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : Source) (mode : RoundingMode) (saturation : SaturationMode) : Format.SameDatum (unary (Destination.p3109 format) operation value mode saturation).decode (format.projectRatValue { rounding := mode, saturation := saturation } (operation (decode value)))

An arbitrary mixed unary operation refines the same destination projection.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.decode_binary {Left LeftExact Right RightExact : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (format : Format) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) (mode : RoundingMode) (saturation : SaturationMode) : Format.SameDatum (binary (Destination.p3109 format) operation left right mode saturation).decode (format.projectRatValue { rounding := mode, saturation := saturation } (operation (decode left) (decode right)))

Both independently decoded operands reach the exact closed operation before projection.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.decode_ternary {Left LeftExact Right RightExact Third ThirdExact : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (format : Format) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) (third : Third) (mode : RoundingMode) (saturation : SaturationMode) : Format.SameDatum (ternary (Destination.p3109 format) operation left right third mode saturation).decode (format.projectRatValue { rounding := mode, saturation := saturation } (operation (decode left) (decode right) (decode third)))

Ternary arithmetic retains all three exact source observations before projection.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.fma_eq_project_finite {Left LeftExact Right RightExact Third ThirdExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (destination : Destination Result) (left : Left) (right : Right) (third : Third) (mode : RoundingMode) (saturation : SaturationMode) (x y z : ℚ) (hx : decode left = Numerics.NumericalValue.finite x) (hy : decode right = Numerics.NumericalValue.finite y) (hz : decode third = Numerics.NumericalValue.finite z) : fma destination left right third mode saturation = destination.project { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (x * y + z))

Finite mixed FMA passes the exact x * y + z to the destination, with no rounded product.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.faa_eq_project_finite {Left LeftExact Right RightExact Third ThirdExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (destination : Destination Result) (left : Left) (middle : Right) (right : Third) (mode : RoundingMode) (saturation : SaturationMode) (x y z : ℚ) (hx : decode left = Numerics.NumericalValue.finite x) (hy : decode middle = Numerics.NumericalValue.finite y) (hz : decode right = Numerics.NumericalValue.finite z) : faa destination left middle right mode saturation = destination.project { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (x + y + z))

Finite mixed FAA passes the exact sum of all three operands to the destination.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.decode_scaledBinary {Left LeftExact Right RightExact : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (format : Format) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode) (saturation : SaturationMode) : Format.SameDatum (scaledBinary (Destination.p3109 format) operation leftScale left rightScale right mode saturation).decode (format.projectRatValue { rounding := mode, saturation := saturation } (operation (Arithmetic.mul (decode leftScale) (decode left)) (Arithmetic.mul (decode rightScale) (decode right))))

Scaled operations project the closed operation on exact block-decoded operands.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledAdd_eq_project_finite {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode) (saturation : SaturationMode) (s x t y : ℚ) (hs : decode leftScale = Numerics.NumericalValue.finite s) (hx : decode left = Numerics.NumericalValue.finite x) (ht : decode rightScale = Numerics.NumericalValue.finite t) (hy : decode right = Numerics.NumericalValue.finite y) : scaledAdd destination leftScale left rightScale right mode saturation = destination.project { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (s * x + t * y))

Finite scaled addition is the projection of s * x + t * y.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledSub_eq_project_finite {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode) (saturation : SaturationMode) (s x t y : ℚ) (hs : decode leftScale = Numerics.NumericalValue.finite s) (hx : decode left = Numerics.NumericalValue.finite x) (ht : decode rightScale = Numerics.NumericalValue.finite t) (hy : decode right = Numerics.NumericalValue.finite y) : scaledSub destination leftScale left rightScale right mode saturation = destination.project { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (s * x - t * y))

Finite scaled subtraction is the projection of s * x - t * y.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledMul_eq_project_finite {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode) (saturation : SaturationMode) (s x t y : ℚ) (hs : decode leftScale = Numerics.NumericalValue.finite s) (hx : decode left = Numerics.NumericalValue.finite x) (ht : decode rightScale = Numerics.NumericalValue.finite t) (hy : decode right = Numerics.NumericalValue.finite y) : scaledMul destination leftScale left rightScale right mode saturation = destination.project { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (s * x * (t * y)))

Finite scaled multiplication retains both scale products before the final projection.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.div_one (value : Numerics.NumericalValue ℚ) : Arithmetic.div value (Numerics.NumericalValue.finite 1) = canonical value

Dividing by the implicit exact result scale one leaves a canonical closed datum unchanged.