Real and complex semantics of ExecComplex

The component map toComplex interprets finite executable values as mathematical complex numbers. Addition and subtraction round each component once. Multiplication records all six rounding sites: four scalar products, the subtraction forming the real component, and the addition forming the imaginary component. Each intermediate rounding appears in the corresponding theorem.

Division records the chosen component ratio and every subsequent rounding. Squared magnitude records two rounded squares and their rounded sum; magnitude applies this to scaled components. Neither an exact field operation nor a whole-operation error bound is asserted.

The finiteness assumptions rule out overflow to infinity and NaN. They are explicit because the real-number semantics does not assign real values to infinities or NaNs.

Reference

• N. J. Higham, Accuracy and Stability of Numerical Algorithms, second edition, SIAM, 2002, Section 3.6. https://doi.org/10.1137/1.9780898718027
• IEEE Standard for Floating-Point Arithmetic, IEEE 754-2019. https://doi.org/10.1109/IEEESTD.2019.8766229

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex {fmt : FloatFormat} (z : ExecComplex fmt) : ℂ

Interpret both finite components as real numbers and assemble a mathematical complex value.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.roundedAdd (fmt : FloatFormat) (x y : ℂ) : ℂ

Componentwise nearest-even semantics for complex addition.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.roundedSub (fmt : FloatFormat) (x y : ℂ) : ℂ

Componentwise nearest-even semantics for complex subtraction.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.roundedMul (fmt : FloatFormat) (x y : ℂ) : ℂ

The rounded real semantics of the evaluation order used by ExecComplex.mul.

This is not exact complex multiplication: each product is rounded before the final rounded subtraction or addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex_neg {fmt : FloatFormat} (z : ExecComplex fmt) (hz : z.isFinite = true) : (-z).toComplex = -z.toComplex

Negation of finite executable components agrees exactly with complex negation.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex_conj {fmt : FloatFormat} (z : ExecComplex fmt) (hz : z.isFinite = true) : z.conj.toComplex = (starRingEnd ℂ) z.toComplex

Complex conjugation is exact on finite components, including formats with unsigned zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex_add_eq_roundedAdd {fmt : FloatFormat} (x y : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : (x + y).isFinite = true) : (x + y).toComplex = roundedAdd fmt x.toComplex y.toComplex

Executable complex addition refines componentwise rounded mathematical addition.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex_sub_eq_roundedSub {fmt : FloatFormat} (x y : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hout : (x - y).isFinite = true) : (x - y).toComplex = roundedSub fmt x.toComplex y.toComplex

Executable complex subtraction refines componentwise rounded mathematical subtraction.

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.MulFinite {fmt : FloatFormat} (x y : ExecComplex fmt) : Prop

All scalar intermediates required to interpret one executable complex multiplication over ℝ.

The predicate includes finite inputs, four finite component products, and finite final components. It is the natural domain of the exact evaluation-order refinement theorem below.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex_mul_eq_roundedMul {fmt : FloatFormat} (x y : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (h : x.MulFinite y) : (x * y).toComplex = roundedMul fmt x.toComplex y.toComplex

For an IEEE descriptor and finite inputs, intermediate values, and result, complex multiplication agrees with roundedMul: four rounded products followed by a rounded subtraction and addition.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.roundedNormSq (fmt : FloatFormat) (z : ℂ) : ℝ

Two separately rounded squares followed by a rounded sum.

structure FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.NormSqFinite {fmt : FloatFormat} (z : ExecComplex fmt) : Prop

Finite inputs, both rounded squares, and their rounded sum.

• input : z.isFinite = true

  Both input components are finite.

• re_square : (z.re.mul z.re).isFinite = true

  The rounded real square is finite.

• im_square : (z.im.mul z.im).isFinite = true

  The rounded imaginary square is finite.

• result : z.normSq.isFinite = true

  The rounded sum is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toReal_normSq_eq_roundedNormSq {fmt : FloatFormat} (z : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (h : z.NormSqFinite) : z.normSq.toReal = roundedNormSq fmt z.toComplex

Squared magnitude agrees with its three scalar rounding sites, including underflow.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.imagDominant_eq_true_iff {fmt : FloatFormat} (z : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (hz : z.isFinite = true) : imagDominant z = true ↔ |z.toComplex.re| < |z.toComplex.im|

The executable pivot comparison agrees with the exact component magnitudes.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.isFinite_magnitudeScale {fmt : FloatFormat} (z : ExecComplex fmt) (hz : z.isFinite = true) : (magnitudeScale z).isFinite = true

Selecting a component and clearing its sign preserves finiteness.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.toReal_magnitudeScale {fmt : FloatFormat} (z : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (hz : z.isFinite = true) : (magnitudeScale z).toReal = max |z.toComplex.re| |z.toComplex.im|

For a finite IEEE complex value, the common scale is the larger absolute component.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.roundedDivRealDominant (fmt : FloatFormat) (x y : ℂ) : ℂ

The nine scalar rounding sites of ratio division with a real-component pivot.

structure FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.DivBranchFinite {fmt : FloatFormat} (x y : ExecComplex fmt) : Prop

Scalar domain obligations for the selected branch of ratio division.

• pivot_nonzero : y.re.isZero = false

  The pivot used to form the ratio is nonzero.

• ratio : (y.im.div y.re).isFinite = true

  The rounded component ratio is finite.

• denominator_product : (y.im.mul (y.im.div y.re)).isFinite = true

  The product used to form the denominator is finite.

• denominator : (y.re.add (y.im.mul (y.im.div y.re))).isFinite = true

  The rounded denominator is finite.

• denominator_nonzero : (y.re.add (y.im.mul (y.im.div y.re))).isZero = false

  The rounded denominator used by both final divisions is nonzero.

• re_product : (x.im.mul (y.im.div y.re)).isFinite = true

  The product used in the real numerator is finite.

• im_product : (x.re.mul (y.im.div y.re)).isFinite = true

  The product used in the imaginary numerator is finite.

• re_numerator : (x.re.add (x.im.mul (y.im.div y.re))).isFinite = true

  The rounded real numerator is finite.

• im_numerator : (x.im.sub (x.re.mul (y.im.div y.re))).isFinite = true

  The rounded imaginary numerator is finite.

• result : (divRealDominant x y).isFinite = true

  Both final quotients are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.toComplex_divRealDominant {fmt : FloatFormat} (x y : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (h : DivBranchFinite x y) : (divRealDominant x y).toComplex = roundedDivRealDominant fmt x.toComplex y.toComplex

The real-pivot division branch evaluates its stated rounded expression when the IEEE inputs and all scalar intermediates are finite, and both the pivot and rounded denominator are nonzero.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.roundedDiv (fmt : FloatFormat) (x y : ℂ) : ℂ

Ratio-division semantics, branching on the exact magnitudes of the denominator components.

In the imaginary-dominant branch the final rounded quotient is conjugated, as in the executable code. This is a rounded expression, not exact division in ℂ.

structure FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.DivFinite {fmt : FloatFormat} (x y : ExecComplex fmt) : Prop

Finite inputs and all scalar domain obligations in the selected division branch.

The pivot and the rounded denominator must both be nonzero; every intermediate and both final quotients must be finite. No obligation is imposed on the branch that is not executed.

• left : x.isFinite = true

  Both numerator components are finite.

• right : y.isFinite = true

  Both denominator components are finite.

• branch : if Internal.imagDominant y = true then Internal.DivBranchFinite (Internal.swap x) (Internal.swap y) else Internal.DivBranchFinite x y

  Domain obligations after choosing the larger denominator component as pivot.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.isFinite_div {fmt : FloatFormat} (x y : ExecComplex fmt) (h : x.DivFinite y) : (x / y).isFinite = true

The selected division branch produces finite components under DivFinite.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toComplex_div_eq_roundedDiv {fmt : FloatFormat} (x y : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (h : x.DivFinite y) : (x / y).toComplex = roundedDiv fmt x.toComplex y.toComplex

Division agrees with the selected ratio formula and all nine scalar rounding sites.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.magnitude_eq_posInf_of_isInf {fmt : FloatFormat} (z : ExecComplex fmt) (hre : z.re.isSNaN = false) (him : z.im.isSNaN = false) (hinf : z.re.isInf = true ∨ z.im.isInf = true) : z.magnitude = Model.posInf fmt

Infinity determines magnitude when neither component is a signaling NaN.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.roundedMagnitude (fmt : FloatFormat) (z : ℂ) : ℝ

Rounded semantics of magnitude with the exact scale max |re| |im|.

The two divisions, two squares, sum, square root, and rescaling product each round separately. Zero scale returns zero without any division.

structure FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.MagnitudeFinite {fmt : FloatFormat} (z : ExecComplex fmt) : Prop

Finite input and output of scaled magnitude, with obligations only on the nonzero-scale branch.

The rounded component ratios, their squares, and their sum must be finite. The sum must be a valid scalar square-root input (zero of either sign, or a clear sign bit). Square-root finiteness then follows from the scalar theorem.

These intermediate-range conditions do not follow merely from finite inputs or from the exact norm fitting in the format. The semantic theorem separately requires the conventional IEEE bias.

• input : z.isFinite = true

  Both input components are finite.

• result : z.magnitude.isFinite = true

  Restoring the scale gives a finite result.

• scaled : (Internal.magnitudeScale z).isZero = false → (Internal.magnitudeRatios z).NormSqFinite ∧ ((Internal.magnitudeRatios z).normSq.isZero = true ∨ (Internal.magnitudeRatios z).normSq.signBit = false)

  Scaled squares and square-root domain, needed only for a nonzero scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.toReal_magnitude_eq_roundedMagnitude {fmt : FloatFormat} (z : ExecComplex fmt) (hfmt : fmt.isIEEE = true) (h : z.MagnitudeFinite) : z.magnitude.toReal = roundedMagnitude fmt z.toComplex

Scaled magnitude agrees with its seven scalar rounding sites, or the zero branch.