Executable exact-dyadic arithmetic

These routines compute exact multiplication, addition, subtraction, and fused multiply-add before any target-format rounding occurs. Record entry points are convenient in specifications; matching field-level entry points let packed decoders reuse the same semantics without constructing short-lived input records.

The representation is not normalized after every operation. Alignment uses the smaller exponent, which leaves normalization to the target-format rounder. Proof establishes that the field-level operations agree with their record-based counterparts and preserve rational denotation.

@[inline]

def FloatLib.Numerics.Dyadic.mulFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Dyadic

Exact product from scalar dyadic fields.

Packed decoders expose these fields individually. Keeping this operation below the record boundary lets verified execution kernels avoid allocating two short-lived input records while returning the same single exact result consumed by rounding.

@[inline]

def FloatLib.Numerics.Dyadic.mul (left right : Dyadic) : Dyadic

Exact product of two dyadic values.

@[inline]

def FloatLib.Numerics.Dyadic.addFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Dyadic

Exact addition from scalar dyadic fields by alignment at the smaller exponent.

If the mathematical sum is zero, the result retains a negative sign only when both operands were negative. This agrees with the usual nearest-even signed-zero convention while remaining harmless for formats, such as posits, that have a unique zero.

@[inline]

def FloatLib.Numerics.Dyadic.add (left right : Dyadic) : Dyadic

Exact addition of two dyadic values.

@[inline]

def FloatLib.Numerics.Dyadic.sumSquares (left right : Dyadic) : Dyadic

Exact sum of two squares, using only natural-number significands.

Both squares are nonnegative, so alignment needs no signed addition or absolute-value recovery. The result has the same fields as exact multiplication followed by addition, including when one or both inputs are zero.

@[inline]

def FloatLib.Numerics.Dyadic.subFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Dyadic

Exact subtraction from scalar dyadic fields.

@[inline]

def FloatLib.Numerics.Dyadic.sub (left right : Dyadic) : Dyadic

Exact subtraction, expressed through exact negation and addition.

@[inline]

def FloatLib.Numerics.Dyadic.fmaFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : ℕ) (addendExponent : ℤ) : Dyadic

Exact fused multiply-add from scalar dyadic fields.

The product is never rounded before addition. Only the single returned exact dyadic is intended to cross into a format-specific rounder.