Exact dyadic values

A FloatLib.Numerics.Dyadic stores a sign, natural significand, and integral power-of-two scale. Arithmetic and rounding can work on these fields without rational normalization.

Lean core's _root_.Dyadic, defined in Init.Data.Dyadic.Basic, normalizes nonzero values to an odd integer times a power of two and has a single zero. The FloatLib record retains an unnormalized significand and scale, together with a separate sign for IEEE signed-zero rules. Its toRat identifies both zero signs; formats with a single zero discard that sign on encoding. toCore converts to Lean's normalized carrier and preserves the rational value.

The carrier provides integer conversions and rational denotation. Arithmetic and order follow in their respective modules.

structure FloatLib.Numerics.Dyadic : Type

An exact signed integer multiple of an integral power of two.

significand = 0 denotes zero for every sign and exponent. Families that distinguish signed zero can preserve that distinction in their semantics and rounding rules; toRat identifies both zeros.

• negative : Bool

  true means negative.

• significand : ℕ

  Nonnegative integer significand.

• exponent : ℤ

  Integral power-of-two scale.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqDyadic : DecidableEq Dyadic

def FloatLib.Numerics.instDecidableEqDyadic.decEq (x✝ x✝¹ : Dyadic) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instReprDyadic : Repr Dyadic

def FloatLib.Numerics.instReprDyadic.repr : Dyadic → ℕ → Std.Format

theorem FloatLib.Numerics.Dyadic.ext {left right : Dyadic} (hnegative : left.negative = right.negative) (hsignificand : left.significand = right.significand) (hexponent : left.exponent = right.exponent) : left = right

Exact dyadics are equal when all three stored scalar fields are equal.

theorem FloatLib.Numerics.Dyadic.ext_iff {left right : Dyadic} : left = right ↔ left.negative = right.negative ∧ left.significand = right.significand ∧ left.exponent = right.exponent

@[inline]

def FloatLib.Numerics.Dyadic.zero : Dyadic

Exact zero with the conventional nonnegative canonical fields.

@[simp]

theorem FloatLib.Numerics.Dyadic.zero_negative : zero.negative = false

Canonical exact zero has a nonnegative sign field.

@[simp]

theorem FloatLib.Numerics.Dyadic.zero_significand : zero.significand = 0

Canonical exact zero has a zero significand.

@[simp]

theorem FloatLib.Numerics.Dyadic.zero_exponent : zero.exponent = 0

Canonical exact zero uses exponent zero.

@[inline]

def FloatLib.Numerics.Dyadic.ofScaledInt (coefficient exponent : ℤ) : Dyadic

Represent coefficient * 2 ^ exponent by extracting the integer's sign and magnitude. Fixed-point accumulators use this conversion before rounding, without rational normalization.

@[inline]

def FloatLib.Numerics.Dyadic.signedSignificand (value : Dyadic) : ℤ

Signed integer significand before the power-of-two scale is applied.

@[simp]

theorem FloatLib.Numerics.Dyadic.natAbs_signedSignificand (value : Dyadic) : value.signedSignificand.natAbs = value.significand

Taking the absolute value of the signed significand recovers its stored magnitude.

@[inline]

def FloatLib.Numerics.Dyadic.toRat (value : Dyadic) : ℚ

Exact rational denotation of a dyadic value.

def FloatLib.Numerics.Dyadic.toCore (value : Dyadic) : _root_.Dyadic

Normalize into Lean's dyadic carrier, identifying the two representations of zero.

@[simp]

theorem FloatLib.Numerics.Dyadic.toRat_toCore (value : Dyadic) : value.toCore.toRat = value.toRat

Converting to Lean's normalized dyadics preserves the exact rational value.

theorem FloatLib.Numerics.Dyadic.toRat_mk_false (significand : ℕ) (exponent : ℤ) : { negative := false, significand := significand, exponent := exponent }.toRat = ↑significand * 2 ^ exponent

A dyadic with a clear sign field denotes its magnitude times its power-of-two scale.

@[simp]

theorem FloatLib.Numerics.Dyadic.toRat_mk_zero (negative : Bool) (exponent : ℤ) : { negative := negative, significand := 0, exponent := exponent }.toRat = 0

Any dyadic record with zero significand denotes rational zero.

@[inline]

def FloatLib.Numerics.Dyadic.neg (value : Dyadic) : Dyadic

Reverse the sign, including the sign of zero. Formats with a single zero apply that policy when encoding the result.

@[simp]

theorem FloatLib.Numerics.Dyadic.neg_eq (value : Dyadic) : value.neg = { negative := !value.negative, significand := value.significand, exponent := value.exponent }

Negation flips only the stored sign field.

@[simp]

theorem FloatLib.Numerics.Dyadic.neg_negative (value : Dyadic) : value.neg.negative = !value.negative

Negation complements the stored sign.

@[simp]

theorem FloatLib.Numerics.Dyadic.neg_significand (value : Dyadic) : value.neg.significand = value.significand

Negation preserves the stored significand.

@[simp]

theorem FloatLib.Numerics.Dyadic.neg_exponent (value : Dyadic) : value.neg.exponent = value.exponent

Negation preserves the stored exponent.