Mathematical semantics of P3109 rational arithmetic

Finite arithmetic is exact rational arithmetic, and rational embedding into the reals preserves the complete expression. The algebraic results describe arithmetic before rounding. The decoding theorems connect the public executable operations to one report projection of that exact result.

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

Exact closed addition is commutative, including exceptional operands.

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

Exact closed multiplication is commutative, including zero times infinity.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.add_assoc (left middle right : Numerics.NumericalValue ℚ) : add (add left middle) right = add left (add middle right)

Exact closed addition is associative; opposite infinities remain indeterminate.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sub_self (value : ℚ) : sub (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite 0

Subtracting a finite datum from itself gives the unique exact zero.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_zero (value : Numerics.NumericalValue ℚ) : div value (Numerics.NumericalValue.finite 0) = nan

Zero denominators are NaN, even for infinite numerators.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_infinity (value : ℚ) (negative : Bool) : div (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.infinity negative) = Numerics.NumericalValue.finite 0

Every finite numerator divided by either infinity gives the unique zero.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_mul_cancel (left right : ℚ) (hright : right ≠ 0) : mul (div (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) (Numerics.NumericalValue.finite right) = Numerics.NumericalValue.finite left

Finite nonzero division cancels before any destination rounding.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.fma_finite (left right addend : ℚ) : fma (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) (Numerics.NumericalValue.finite addend) = Numerics.NumericalValue.finite (left * right + addend)

Finite fused multiply-add retains the whole rational expression.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.faa_eq_add_add (left middle right : Numerics.NumericalValue ℚ) : faa left middle right = add left (add middle right)

Fused add-add is independent of the grouping of the exact additions.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.add_finite_real (left right : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (add (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left + ↑right)

Rational addition embeds as addition in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sub_finite_real (left right : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (sub (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left - ↑right)

Rational subtraction embeds as subtraction in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.mul_finite_real (left right : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (mul (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left * ↑right)

Rational multiplication embeds as multiplication in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_finite_real (left right : ℚ) (hright : right ≠ 0) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (div (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left / ↑right)

Nonzero rational division embeds as division in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.fma_finite_real (left right addend : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (fma (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) (Numerics.NumericalValue.finite addend)) = Numerics.NumericalValue.finite (↑left * ↑right + ↑addend)

FMA computes the real expression with no rounded intermediate product.

theorem FloatLib.Floats.ExecFloat.P3109.decode_unaryTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : P3109 source) : Formats.P3109.Format.SameDatum (unaryTo destination policy operation value).decode (destination.projectRatValue policy (operation value.toClosedRat))

The executable unary operation decodes to one projection of its exact closed result.

theorem FloatLib.Floats.ExecFloat.P3109.decode_binaryTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) : Formats.P3109.Format.SameDatum (binaryTo destination policy operation left right).decode (destination.projectRatValue policy (operation left.toClosedRat right.toClosedRat))

The executable binary operation decodes to one projection of its exact closed result.

theorem FloatLib.Floats.ExecFloat.P3109.decode_ternaryTo {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) (third : P3109 thirdFormat) : Formats.P3109.Format.SameDatum (ternaryTo destination policy operation left right third).decode (destination.projectRatValue policy (operation left.toClosedRat right.toClosedRat third.toClosedRat))

The executable fused operation decodes to one projection of the whole exact expression.

theorem FloatLib.Floats.ExecFloat.P3109.decode_fmaTo_finite {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (left : P3109 leftFormat) (right : P3109 rightFormat) (addend : P3109 thirdFormat) (x y z : ℚ) (hleft : left.toClosedRat = Numerics.NumericalValue.finite x) (hright : right.toClosedRat = Numerics.NumericalValue.finite y) (haddend : addend.toClosedRat = Numerics.NumericalValue.finite z) : Formats.P3109.Format.SameDatum (fmaTo destination policy left right addend).decode (destination.projectRatValue policy (Numerics.NumericalValue.finite (x * y + z)))

Finite FMA is one projection of the exact rational product plus addend.