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 retains 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) (policy : ProjectionPolicy) (value : Source) : Format.SameDatum (convert (Destination.p3109 format) policy value).decode (format.projectRatValue policy (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) (policy : ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : Source) : Format.SameDatum (unary (Destination.p3109 format) policy operation value).decode (format.projectRatValue policy (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) (policy : ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) : Format.SameDatum (binary (Destination.p3109 format) policy operation left right).decode (format.projectRatValue policy (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) (policy : ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) (third : Third) : Format.SameDatum (ternary (Destination.p3109 format) policy operation left right third).decode (format.projectRatValue policy (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) (policy : ProjectionPolicy) (left : Left) (right : Right) (third : Third) (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 policy left right third = destination.project policy (Numerics.NumericalValue.finite (x * y + z))

Finite mixed FMA passes exactly x * y + z to the destination, without a 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) (policy : ProjectionPolicy) (left : Left) (middle : Right) (right : Third) (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 policy left middle right = destination.project policy (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) (policy : ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) : Format.SameDatum (scaledBinary (Destination.p3109 format) policy operation leftScale left rightScale right).decode (format.projectRatValue policy (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) (policy : ProjectionPolicy) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (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 policy leftScale left rightScale right = destination.project policy (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) (policy : ProjectionPolicy) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (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 policy leftScale left rightScale right = destination.project policy (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) (policy : ProjectionPolicy) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (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 policy leftScale left rightScale right = destination.project policy (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.