Rational semantics of dyadic arithmetic

Field-level multiplication and fused multiply-add agree with their record-based expressions. Addition and subtraction preserve rational denotation, including when the exact result is zero.

For addition, align the operands at the smaller exponent and add their signed integer significands. The main argument shows that recovering the sign and magnitude with natAbs preserves that sum.

Field-level operations

theorem FloatLib.Numerics.Dyadic.mul_eq (left right : Dyadic) : left.mul right = { negative := left.negative ^^ right.negative, significand := left.significand * right.significand, exponent := left.exponent + right.exponent }

Multiplication combines the three stored dyadic fields independently.

@[simp]

theorem FloatLib.Numerics.Dyadic.mul_negative (left right : Dyadic) : (left.mul right).negative = (left.negative ^^ right.negative)

Multiplication combines stored signs by exclusive-or.

@[simp]

theorem FloatLib.Numerics.Dyadic.mul_significand (left right : Dyadic) : (left.mul right).significand = left.significand * right.significand

Multiplication multiplies the stored significands.

@[simp]

theorem FloatLib.Numerics.Dyadic.mul_exponent (left right : Dyadic) : (left.mul right).exponent = left.exponent + right.exponent

Multiplication adds the stored binary exponents.

theorem FloatLib.Numerics.Dyadic.mulFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : mulFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.mul { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Scalar-field multiplication is exactly record-based dyadic multiplication.

theorem FloatLib.Numerics.Dyadic.addFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : addFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.add { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Scalar-field addition is exactly record-based dyadic addition.

theorem FloatLib.Numerics.Dyadic.subFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : subFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.sub { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Scalar-field subtraction is exactly record-based dyadic subtraction.

theorem FloatLib.Numerics.Dyadic.fmaFields_eq (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) (addendNegative : Bool) (addendSignificand : ℕ) (addendExponent : ℤ) : fmaFields leftNegative leftSignificand leftExponent rightNegative rightSignificand rightExponent addendNegative addendSignificand addendExponent = ({ negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.mul { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }).add { negative := addendNegative, significand := addendSignificand, exponent := addendExponent }

Scalar-field FMA is multiplication followed by exact addition, with no intermediate rounding.

Structural addition laws

@[simp]

theorem FloatLib.Numerics.Dyadic.add_of_left_significand_eq_zero (left right : Dyadic) (hleft : left.significand = 0) : left.add right = if right.significand = 0 then { negative := left.negative && right.negative, significand := 0, exponent := 0 } else right

Normalize addition when the left operand stores zero.

A nonzero right operand is returned unchanged. If both operands store zero, the result uses the canonical zero exponent and the shared signed-zero rule. In either case the left exponent is irrelevant.

@[simp]

theorem FloatLib.Numerics.Dyadic.add_of_right_significand_eq_zero (left right : Dyadic) (hright : right.significand = 0) : left.add right = if left.significand = 0 then { negative := left.negative && right.negative, significand := 0, exponent := 0 } else left

Normalize addition when the right operand stores zero.

This is the symmetric form of add_of_left_significand_eq_zero; in particular, the right exponent never affects the result.

theorem FloatLib.Numerics.Dyadic.add_of_significands_eq_zero (left right : Dyadic) (hleft : left.significand = 0) (hright : right.significand = 0) : left.add right = { negative := left.negative && right.negative, significand := 0, exponent := 0 }

Adding two stored zeros returns the canonical zero exponent and preserves a negative sign only when both inputs are negative.

theorem FloatLib.Numerics.Dyadic.add_same_sign_same_exponent (sign : Bool) (left right : ℕ) (exponent : ℤ) (hleft : left ≠ 0) (hright : right ≠ 0) : { negative := sign, significand := left, exponent := exponent }.add { negative := sign, significand := right, exponent := exponent } = { negative := sign, significand := left + right, exponent := exponent }

Equal-exponent, same-sign addition only adds the two nonzero significands.

theorem FloatLib.Numerics.Dyadic.add_opposite_sign_same_exponent_large_left (largeSign smallSign : Bool) (large small : ℕ) (exponent : ℤ) (hlarge : large ≠ 0) (hsmall : small ≠ 0) (hsign : largeSign ≠ smallSign) (hlt : small < large) : { negative := largeSign, significand := large, exponent := exponent }.add { negative := smallSign, significand := small, exponent := exponent } = { negative := largeSign, significand := large - small, exponent := exponent }

At a shared exponent, opposite signs subtract magnitudes and retain the sign of the larger left operand.

theorem FloatLib.Numerics.Dyadic.add_comm (left right : Dyadic) : left.add right = right.add left

Exact addition is structurally commutative, including the signed-zero convention.

This is stronger than commutativity of rational denotation: both sides produce the same stored zero sign and exponent.

theorem FloatLib.Numerics.Dyadic.add_opposite_sign_same_exponent_large_right (smallSign largeSign : Bool) (small large : ℕ) (exponent : ℤ) (hsmall : small ≠ 0) (hlarge : large ≠ 0) (hsign : smallSign ≠ largeSign) (hlt : small < large) : { negative := smallSign, significand := small, exponent := exponent }.add { negative := largeSign, significand := large, exponent := exponent } = { negative := largeSign, significand := large - small, exponent := exponent }

At a shared exponent, opposite signs subtract magnitudes and retain the sign of the larger right operand.

theorem FloatLib.Numerics.Dyadic.add_opposite_sign_same_exponent_eq_zero (leftSign rightSign : Bool) (magnitude : ℕ) (exponent : ℤ) (hmagnitude : magnitude ≠ 0) (hsign : leftSign ≠ rightSign) : { negative := leftSign, significand := magnitude, exponent := exponent }.add { negative := rightSign, significand := magnitude, exponent := exponent } = { negative := false, significand := 0, exponent := 0 }

Equal nonzero magnitudes with opposite signs cancel to canonical positive zero.

theorem FloatLib.Numerics.Dyadic.add_align_right_to_left_exponent (leftNegative rightNegative : Bool) (leftSignificand rightSignificand : ℕ) (leftExponent rightExponent : ℤ) (hleft : leftSignificand ≠ 0) (hright : rightSignificand ≠ 0) (hexponents : leftExponent ≤ rightExponent) : { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.add { negative := rightNegative, significand := rightSignificand, exponent := rightExponent } = { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.add { negative := rightNegative, significand := rightSignificand.shiftLeft (rightExponent - leftExponent).toNat, exponent := leftExponent }

Align a nonzero right operand at the smaller left exponent before exact addition.

This is the mathematical bridge used by bounded-word kernels that perform the shift explicitly.

theorem FloatLib.Numerics.Dyadic.add_align_left_to_right_exponent (leftNegative rightNegative : Bool) (leftSignificand rightSignificand : ℕ) (leftExponent rightExponent : ℤ) (hleft : leftSignificand ≠ 0) (hright : rightSignificand ≠ 0) (hexponents : rightExponent < leftExponent) : { negative := leftNegative, significand := leftSignificand, exponent := leftExponent }.add { negative := rightNegative, significand := rightSignificand, exponent := rightExponent } = { negative := leftNegative, significand := leftSignificand.shiftLeft (leftExponent - rightExponent).toNat, exponent := rightExponent }.add { negative := rightNegative, significand := rightSignificand, exponent := rightExponent }

Align a nonzero left operand at the smaller right exponent before exact addition.

theorem FloatLib.Numerics.Dyadic.add_opposite_sign_adjacent_exponent_large_left (largeSign smallSign : Bool) (large small : ℕ) (exponent : ℤ) (hlarge : large ≠ 0) (hsmall : small ≠ 0) (hsign : largeSign ≠ smallSign) (hlt : small < large.shiftLeft 1) : { negative := largeSign, significand := large, exponent := exponent + 1 }.add { negative := smallSign, significand := small, exponent := exponent } = { negative := largeSign, significand := large.shiftLeft 1 - small, exponent := exponent }

Subtract an opposite-sign magnitude one exponent below a larger left operand.

Alignment doubles the higher-exponent significand, after which this is ordinary equal-exponent subtraction. The theorem is independent of any concrete floating-point width.

theorem FloatLib.Numerics.Dyadic.add_opposite_sign_adjacent_exponent_large_right (smallSign largeSign : Bool) (small large : ℕ) (exponent : ℤ) (hsmall : small ≠ 0) (hlarge : large ≠ 0) (hsign : smallSign ≠ largeSign) (hlt : small < large.shiftLeft 1) : { negative := smallSign, significand := small, exponent := exponent }.add { negative := largeSign, significand := large, exponent := exponent + 1 } = { negative := largeSign, significand := large.shiftLeft 1 - small, exponent := exponent }

Symmetric adjacent-exponent subtraction with the larger magnitude on the right.

Rational denotation of aligned arithmetic

Public arithmetic contracts

theorem FloatLib.Numerics.Dyadic.add_toRat (left right : Dyadic) : (left.add right).toRat = left.toRat + right.toRat

Exact dyadic addition commutes with rational denotation.

theorem FloatLib.Numerics.Dyadic.sub_toRat (left right : Dyadic) : (left.sub right).toRat = left.toRat - right.toRat

Exact dyadic subtraction commutes with rational denotation.

@[simp]

theorem FloatLib.Numerics.Dyadic.mul_zero_left (value : Dyadic) : zero.mul value = { negative := value.negative, significand := 0, exponent := value.exponent }

Multiplying canonical zero on the left returns zero with the other operand's sign and exponent.

@[simp]

theorem FloatLib.Numerics.Dyadic.mul_zero_right (value : Dyadic) : value.mul zero = { negative := value.negative, significand := 0, exponent := value.exponent }

Multiplying canonical zero on the right returns zero with the other operand's sign and exponent.