Executable complex numbers over an arbitrary binary format

ExecComplex fmt stores one Model fmt for each Cartesian component. The format parameter is not fixed to binary32: the same definition supports binary16, bfloat16, binary64, binary128, binary256, and custom exponent/fraction widths.

Complex multiplication uses four scalar multiplications followed by one subtraction and one addition. This explicit evaluation order matters in floating-point arithmetic and is reflected by the semantic theorem in Complex.Semantics.

Division uses the larger denominator component to form a ratio. Magnitude scales both components before squaring. These evaluation orders avoid squaring large unscaled components, but do not guarantee finite intermediates or correct rounding of the exact complex operation.

structure FloatLib.Floats.Formats.BinaryInterchange.ExecComplex (fmt : FloatFormat) : Type

A complex value whose real and imaginary components share the binary format fmt.

• re : Model fmt

  Real component.

• im : Model fmt

  Imaginary component.

def FloatLib.Floats.Formats.BinaryInterchange.instDecidableEqExecComplex.decEq {fmt✝ : FloatFormat} (x✝ x✝¹ : ExecComplex fmt✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instDecidableEqExecComplex {fmt✝ : FloatFormat} : DecidableEq (ExecComplex fmt✝)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.instReprExecComplex {fmt✝ : FloatFormat} : Repr (ExecComplex fmt✝)

def FloatLib.Floats.Formats.BinaryInterchange.instReprExecComplex.repr {fmt✝ : FloatFormat} : ExecComplex fmt✝ → ℕ → Std.Format

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.isFinite {fmt : FloatFormat} (z : ExecComplex fmt) : Bool

A complex value is finite exactly when both encoded components are finite.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.neg {fmt : FloatFormat} (z : ExecComplex fmt) : ExecComplex fmt

Componentwise sign negation.

@[inline]

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

Componentwise floating-point addition.

@[inline]

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

Componentwise floating-point subtraction.

@[noinline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.mulReal {fmt : FloatFormat} (x y : ExecComplex fmt) : Model fmt

Real component of the specified non-fused complex product.

@[noinline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.mulImag {fmt : FloatFormat} (x y : ExecComplex fmt) : Model fmt

Imaginary component of the specified non-fused complex product.

@[inline]

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

Floating-point complex multiplication with an explicit non-fused evaluation order.

Each of the four component products is rounded in fmt; the real subtraction and imaginary addition are then rounded once more in the same format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.conj {fmt : FloatFormat} (z : ExecComplex fmt) : ExecComplex fmt

Conjugation negates the imaginary component using the format's zero and NaN conventions.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.normSq {fmt : FloatFormat} (z : ExecComplex fmt) : Model fmt

Squared magnitude with two rounded squares followed by a rounded sum.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.swap {fmt : FloatFormat} (z : ExecComplex fmt) : ExecComplex fmt

Exchange the real and imaginary coordinates.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.imagDominant {fmt : FloatFormat} (z : ExecComplex fmt) : Bool

The strict comparison chooses the real component on a tie or an unordered comparison.

@[inline]

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

Ratio division with the real denominator component as pivot.

Every multiplication, sum, difference, and quotient is rounded separately.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.magnitudeScale {fmt : FloatFormat} (z : ExecComplex fmt) : Model fmt

Larger component magnitude, with the real component selected on ties.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.Internal.magnitudeRatios {fmt : FloatFormat} (z : ExecComplex fmt) : ExecComplex fmt

Components divided by their common magnitude scale, each rounded once.

@[inline]

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

Complex division by a component-ratio formula.

When the imaginary denominator component is larger, both inputs exchange coordinates and the computed quotient is conjugated. This includes an exact sign change after the final imaginary division. Scalar kernels determine exceptional results; there is no complex infinity recovery. Finite inputs alone do not exclude overflow, underflow, or a zero rounded denominator.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.magnitude {fmt : FloatFormat} (z : ExecComplex fmt) : Model fmt

Magnitude computed by scaling before squaring and restoring the scale after square root.

A zero scale returns positive zero on finite IEEE inputs. All finite arithmetic uses the component kernels; the result need not be one rounding of the exact norm. An infinite component gives positive infinity even when the other component is a quiet NaN. If either component is a signaling NaN, or neither is infinite, nonfinite inputs use the scalar sum of absolute components and its NaN selection and quieting policy.

The format must also have enough range for the normalized intermediate sum. For example, FloatFormat.custom 2 2 2 .ieee maps (0.5, 0.5) to infinity because the normalized sum 2 overflows, although the nearest rounded exact norm is 0.75. This custom bias also fails fmt.isIEEE; the finite rounded-semantics theorem does not apply.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.instNeg {fmt : FloatFormat} : Neg (ExecComplex fmt)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.instAdd {fmt : FloatFormat} : Add (ExecComplex fmt)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.instSub {fmt : FloatFormat} : Sub (ExecComplex fmt)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.instMul {fmt : FloatFormat} : Mul (ExecComplex fmt)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.instDiv {fmt : FloatFormat} : Div (ExecComplex fmt)

theorem FloatLib.Floats.Formats.BinaryInterchange.ExecComplex.isFinite_eq_true_iff {fmt : FloatFormat} (z : ExecComplex fmt) : z.isFinite = true ↔ z.re.isFinite = true ∧ z.im.isFinite = true

Boolean finiteness separates into the corresponding facts for both components.