Dyadic Rationals (n * 2^e)

This file defines Dyadic rationals, which are the backbone of high-performance verified numerics. Unlike arbitrary Rat, Dyadics do not require GCD normalization, making them significantly faster for kernel evaluation.

Main definitions

• Dyadic - A dyadic rational number: mantissa * 2^exponent
• Dyadic.toRat - Convert to standard rational
• Dyadic.add, Dyadic.mul, Dyadic.neg - Arithmetic operations
• Dyadic.shiftDown, Dyadic.shiftUp - Directed rounding for interval bounds

Design notes

Dyadics use power-of-2 multiplications instead of GCD-based normalization. This makes them orders of magnitude faster for kernel evaluation via native_decide, since 2^n can be computed by simple bit operations.

For interval arithmetic, we use directed rounding:

• Lower bounds use shiftDown (round toward -∞)
• Upper bounds use shiftUp (round toward +∞)

This ensures mathematical soundness even when truncating precision.

structure LeanCert.Core.Dyadic : Type

A Dyadic rational number: mantissa * 2^exponent

This representation allows fast arithmetic without GCD normalization.

• mantissa : ℤ

  The significand/mantissa

• exponent : ℤ

  The exponent (power of 2)

instance LeanCert.Core.instReprDyadic : Repr Dyadic

Equations

• LeanCert.Core.instReprDyadic = { reprPrec := LeanCert.Core.instReprDyadic.repr }

def LeanCert.Core.instReprDyadic.repr : Dyadic → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Core.instDecidableEqDyadic : DecidableEq Dyadic

Equations

• LeanCert.Core.instDecidableEqDyadic = LeanCert.Core.instDecidableEqDyadic.decEq

def LeanCert.Core.instDecidableEqDyadic.decEq (x✝ x✝¹ : Dyadic) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Core.instInhabitedDyadic.default : Dyadic

Equations

• LeanCert.Core.instInhabitedDyadic.default = { mantissa := default, exponent := default }

instance LeanCert.Core.instInhabitedDyadic : Inhabited Dyadic

Equations

• LeanCert.Core.instInhabitedDyadic = { default := LeanCert.Core.instInhabitedDyadic.default }

Helper: Power of 2

def LeanCert.Core.Dyadic.pow2Nat (n : ℕ) : ℕ

Compute 2^n for natural n

Equations

• LeanCert.Core.Dyadic.pow2Nat n = Nat.shiftLeft 1 n

def LeanCert.Core.Dyadic.shiftLeftInt (m : ℤ) (n : ℕ) : ℤ

Shift an integer left by n bits (multiply by 2^n)

Equations

• LeanCert.Core.Dyadic.shiftLeftInt m n = m * ↑(LeanCert.Core.Dyadic.pow2Nat n)

def LeanCert.Core.Dyadic.shiftRightInt (m : ℤ) (n : ℕ) : ℤ

Shift an integer right by n bits (divide by 2^n, floor toward -∞)

Equations

• LeanCert.Core.Dyadic.shiftRightInt m n = m / ↑(LeanCert.Core.Dyadic.pow2Nat n)

def LeanCert.Core.Dyadic.hasLowBits (m : ℤ) (n : ℕ) : Bool

Check if any of the low n bits are set

Equations

• LeanCert.Core.Dyadic.hasLowBits m n = decide (m % ↑(LeanCert.Core.Dyadic.pow2Nat n) ≠ 0)

Conversion to Rat

def LeanCert.Core.Dyadic.toRat (d : Dyadic) : ℚ

Convert Dyadic to standard Rat.

For non-negative exponents: mantissa * 2^exponent For negative exponents: mantissa / 2^(-exponent)

Equations

• d.toRat = if d.exponent ≥ 0 then ↑d.mantissa * ↑↑(LeanCert.Core.Dyadic.pow2Nat d.exponent.toNat) else ↑d.mantissa / ↑(LeanCert.Core.Dyadic.pow2Nat (-d.exponent).toNat)

instance LeanCert.Core.Dyadic.instCoeRat : Coe Dyadic ℚ

Equations

• LeanCert.Core.Dyadic.instCoeRat = { coe := LeanCert.Core.Dyadic.toRat }

def LeanCert.Core.Dyadic.toReal (d : Dyadic) : ℝ

Cast a Dyadic to ℝ by going through ℚ

Equations

• d.toReal = ↑d.toRat

instance LeanCert.Core.Dyadic.instCoeReal : Coe Dyadic ℝ

Equations

• LeanCert.Core.Dyadic.instCoeReal = { coe := LeanCert.Core.Dyadic.toReal }

theorem LeanCert.Core.Dyadic.toRat_injective_of_normalized {d₁ d₂ : Dyadic} (h : d₁.toRat = d₂.toRat) : d₁.toRat = d₂.toRat

Two Dyadics are equal as rationals iff their toRat values are equal

Construction

def LeanCert.Core.Dyadic.ofInt (i : ℤ) : Dyadic

Create a dyadic from an integer (exponent = 0)

Equations

• LeanCert.Core.Dyadic.ofInt i = { mantissa := i, exponent := 0 }

def LeanCert.Core.Dyadic.pow2 (n : ℤ) : Dyadic

Create a dyadic for 2^n

Equations

• LeanCert.Core.Dyadic.pow2 n = { mantissa := 1, exponent := n }

def LeanCert.Core.Dyadic.zero : Dyadic

Zero as a Dyadic

Equations

• LeanCert.Core.Dyadic.zero = { mantissa := 0, exponent := 0 }

def LeanCert.Core.Dyadic.one : Dyadic

One as a Dyadic

Equations

• LeanCert.Core.Dyadic.one = { mantissa := 1, exponent := 0 }

instance LeanCert.Core.Dyadic.instZero : Zero Dyadic

Equations

• LeanCert.Core.Dyadic.instZero = { zero := LeanCert.Core.Dyadic.zero }

instance LeanCert.Core.Dyadic.instOne : One Dyadic

Equations

• LeanCert.Core.Dyadic.instOne = { one := LeanCert.Core.Dyadic.one }

@[simp]

theorem LeanCert.Core.Dyadic.toRat_zero : toRat 0 = 0

@[simp]

theorem LeanCert.Core.Dyadic.toRat_one : toRat 1 = 1

theorem LeanCert.Core.Dyadic.toRat_ofInt (i : ℤ) : (ofInt i).toRat = ↑i

Arithmetic Operations

def LeanCert.Core.Dyadic.neg (d : Dyadic) : Dyadic

Negation of a Dyadic

Equations

• d.neg = { mantissa := -d.mantissa, exponent := d.exponent }

instance LeanCert.Core.Dyadic.instNeg : Neg Dyadic

Equations

• LeanCert.Core.Dyadic.instNeg = { neg := LeanCert.Core.Dyadic.neg }

def LeanCert.Core.Dyadic.add (d₁ d₂ : Dyadic) : Dyadic

Addition of Dyadics. Aligns exponents by shifting the mantissa with larger exponent to match the smaller one.

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Core.Dyadic.instAdd : Add Dyadic

Equations

• LeanCert.Core.Dyadic.instAdd = { add := LeanCert.Core.Dyadic.add }

def LeanCert.Core.Dyadic.sub (d₁ d₂ : Dyadic) : Dyadic

Subtraction of Dyadics

Equations

• d₁.sub d₂ = d₁.add d₂.neg

instance LeanCert.Core.Dyadic.instSub : Sub Dyadic

Equations

• LeanCert.Core.Dyadic.instSub = { sub := LeanCert.Core.Dyadic.sub }

def LeanCert.Core.Dyadic.mul (d₁ d₂ : Dyadic) : Dyadic

Multiplication of Dyadics. Simply multiplies mantissas and adds exponents.

Equations

• d₁.mul d₂ = { mantissa := d₁.mantissa * d₂.mantissa, exponent := d₁.exponent + d₂.exponent }

instance LeanCert.Core.Dyadic.instMul : Mul Dyadic

Equations

• LeanCert.Core.Dyadic.instMul = { mul := LeanCert.Core.Dyadic.mul }

def LeanCert.Core.Dyadic.abs (d : Dyadic) : Dyadic

Absolute value of a Dyadic

Equations

• d.abs = { mantissa := ↑d.mantissa.natAbs, exponent := d.exponent }

def LeanCert.Core.Dyadic.scale2 (d : Dyadic) (n : ℤ) : Dyadic

Scale by a power of 2 (efficient: just adjusts exponent)

Equations

• d.scale2 n = { mantissa := d.mantissa, exponent := d.exponent + n }

Directed Rounding for Interval Arithmetic

def LeanCert.Core.Dyadic.shiftDown (d : Dyadic) (newExp : ℤ) : Dyadic

Shift a dyadic to a new (larger) exponent with "Down" rounding (for lower bounds).

If newExp > d.exponent, we lose precision by right-shifting the mantissa. Bits are discarded (floor division toward -∞).

Equations

• d.shiftDown newExp = if newExp ≤ d.exponent then d else have diff := (newExp - d.exponent).toNat; { mantissa := LeanCert.Core.Dyadic.shiftRightInt d.mantissa diff, exponent := newExp }

def LeanCert.Core.Dyadic.shiftUp (d : Dyadic) (newExp : ℤ) : Dyadic

Shift a dyadic to a new (larger) exponent with "Up" rounding (for upper bounds).

If newExp > d.exponent, we lose precision by right-shifting the mantissa. If any bits are lost, we add 1 to ensure upward rounding (ceiling toward +∞).

Equations

• One or more equations did not get rendered due to their size.

Normalization (Mantissa Control)

def LeanCert.Core.Dyadic.bitLength (m : ℤ) : ℕ

Get the bit length of the absolute value of an integer

Equations

• LeanCert.Core.Dyadic.bitLength m = LeanCert.Core.Dyadic.natBitLength✝ m.natAbs

def LeanCert.Core.Dyadic.normalize (d : Dyadic) (maxBits : ℕ := 256) (roundUp : Bool := false) : Dyadic

Normalize a Dyadic to keep the mantissa within a reasonable bit-limit.

This prevents mantissas from growing without bound during repeated multiplications. Similar to how hardware floats work, but with directed rounding.

• maxBits: Maximum allowed bits for mantissa (default 256)
• roundUp: If true, round toward +∞; if false, round toward -∞

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Core.Dyadic.normalizeDown (d : Dyadic) (maxBits : ℕ := 256) : Dyadic

Normalize for lower bounds (round down)

Equations

• d.normalizeDown maxBits = d.normalize maxBits

def LeanCert.Core.Dyadic.normalizeUp (d : Dyadic) (maxBits : ℕ := 256) : Dyadic

Normalize for upper bounds (round up)

Equations

• d.normalizeUp maxBits = d.normalize maxBits true

Comparison

def LeanCert.Core.Dyadic.compare (d₁ d₂ : Dyadic) : Ordering

Compare two Dyadics (decidable)

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Core.Dyadic.instOrd : Ord Dyadic

Equations

• LeanCert.Core.Dyadic.instOrd = { compare := LeanCert.Core.Dyadic.compare }

def LeanCert.Core.Dyadic.le (d₁ d₂ : Dyadic) : Bool

Less-than-or-equal for Dyadics

Equations

• d₁.le d₂ = (d₁.compare d₂ != Ordering.gt)

def LeanCert.Core.Dyadic.lt (d₁ d₂ : Dyadic) : Bool

Less-than for Dyadics

Equations

• d₁.lt d₂ = (d₁.compare d₂ == Ordering.lt)

instance LeanCert.Core.Dyadic.instLE : LE Dyadic

Equations

• LeanCert.Core.Dyadic.instLE = { le := fun (d₁ d₂ : LeanCert.Core.Dyadic) => d₁.le d₂ = true }

instance LeanCert.Core.Dyadic.instLT : LT Dyadic

Equations

• LeanCert.Core.Dyadic.instLT = { lt := fun (d₁ d₂ : LeanCert.Core.Dyadic) => d₁.lt d₂ = true }

instance LeanCert.Core.Dyadic.instDecidableRelLe : DecidableRel fun (x1 x2 : Dyadic) => x1 ≤ x2

Equations

• d₁.instDecidableRelLe d₂ = if h : d₁.le d₂ = true then isTrue h else isFalse h

instance LeanCert.Core.Dyadic.instDecidableRelLt : DecidableRel fun (x1 x2 : Dyadic) => x1 < x2

Equations

• d₁.instDecidableRelLt d₂ = if h : d₁.lt d₂ = true then isTrue h else isFalse h

def LeanCert.Core.Dyadic.min (d₁ d₂ : Dyadic) : Dyadic

Minimum of two Dyadics

Equations

• d₁.min d₂ = if d₁.le d₂ = true then d₁ else d₂

def LeanCert.Core.Dyadic.max (d₁ d₂ : Dyadic) : Dyadic

Maximum of two Dyadics

Equations

• d₁.max d₂ = if d₁.le d₂ = true then d₂ else d₁

def LeanCert.Core.Dyadic.min4 (a b c d : Dyadic) : Dyadic

Minimum of four Dyadics

Equations

• a.min4 b c d = (a.min b).min (c.min d)

def LeanCert.Core.Dyadic.max4 (a b c d : Dyadic) : Dyadic

Maximum of four Dyadics

Equations

• a.max4 b c d = (a.max b).max (c.max d)

Correctness Theorems

Helper lemmas for shift proofs

theorem LeanCert.Core.Dyadic.toRat_neg (d : Dyadic) : d.neg.toRat = -d.toRat

Arithmetic Homomorphisms

theorem LeanCert.Core.Dyadic.toRat_eq (d : Dyadic) : d.toRat = ↑d.mantissa * 2 ^ d.exponent

Unification lemma: toRat d = d.mantissa * 2^d.exponent

theorem LeanCert.Core.Dyadic.toRat_add (d₁ d₂ : Dyadic) : (d₁.add d₂).toRat = d₁.toRat + d₂.toRat

theorem LeanCert.Core.Dyadic.toRat_mul (d₁ d₂ : Dyadic) : (d₁.mul d₂).toRat = d₁.toRat * d₂.toRat

Rounding Properties

theorem LeanCert.Core.Dyadic.toRat_shiftDown_le (d : Dyadic) (newExp : ℤ) : (d.shiftDown newExp).toRat ≤ d.toRat

shiftDown produces a value ≤ the original

theorem LeanCert.Core.Dyadic.toRat_shiftUp_ge (d : Dyadic) (newExp : ℤ) : d.toRat ≤ (d.shiftUp newExp).toRat

shiftUp produces a value ≥ the original

Comparison Helper Lemmas

Comparison Theorems

theorem LeanCert.Core.Dyadic.le_iff_toRat_le (d₁ d₂ : Dyadic) : d₁.le d₂ = true ↔ d₁.toRat ≤ d₂.toRat

le is correct with respect to toRat ordering

theorem LeanCert.Core.Dyadic.compare_lt_iff (d₁ d₂ : Dyadic) : d₁.compare d₂ = Ordering.lt ↔ d₁.toRat < d₂.toRat

compare reflects toRat ordering: lt case

theorem LeanCert.Core.Dyadic.compare_gt_iff (d₁ d₂ : Dyadic) : d₁.compare d₂ = Ordering.gt ↔ d₁.toRat > d₂.toRat

compare reflects toRat ordering: gt case

theorem LeanCert.Core.Dyadic.compare_eq_iff (d₁ d₂ : Dyadic) : d₁.compare d₂ = Ordering.eq ↔ d₁.toRat = d₂.toRat

compare reflects toRat ordering: eq case

Min/Max Lemmas

theorem LeanCert.Core.Dyadic.min_toRat_le_left (d₁ d₂ : Dyadic) : (d₁.min d₂).toRat ≤ d₁.toRat

min produces value ≤ first argument

theorem LeanCert.Core.Dyadic.min_toRat_le_right (d₁ d₂ : Dyadic) : (d₁.min d₂).toRat ≤ d₂.toRat

min produces value ≤ second argument

theorem LeanCert.Core.Dyadic.le_max_toRat_left (d₁ d₂ : Dyadic) : d₁.toRat ≤ (d₁.max d₂).toRat

first argument ≤ max

theorem LeanCert.Core.Dyadic.le_max_toRat_right (d₁ d₂ : Dyadic) : d₂.toRat ≤ (d₁.max d₂).toRat

second argument ≤ max

theorem LeanCert.Core.Dyadic.min_toRat (d₁ d₂ : Dyadic) : (d₁.min d₂).toRat = Min.min d₁.toRat d₂.toRat

Dyadic.min commutes with toRat

theorem LeanCert.Core.Dyadic.max_toRat (d₁ d₂ : Dyadic) : (d₁.max d₂).toRat = Max.max d₁.toRat d₂.toRat

Dyadic.max commutes with toRat

theorem LeanCert.Core.Dyadic.min4_le_max4 (a b c d : Dyadic) : (a.min4 b c d).toRat ≤ (a.max4 b c d).toRat

min4 ≤ max4

Normalize Lemmas

theorem LeanCert.Core.Dyadic.toRat_normalizeDown_le (d : Dyadic) (maxBits : ℕ) : (d.normalizeDown maxBits).toRat ≤ d.toRat

normalizeDown produces value ≤ original

theorem LeanCert.Core.Dyadic.toRat_normalizeUp_ge (d : Dyadic) (maxBits : ℕ) : d.toRat ≤ (d.normalizeUp maxBits).toRat

normalizeUp produces value ≥ original

Scale2 Lemmas

theorem LeanCert.Core.Dyadic.toRat_scale2 (d : Dyadic) (n : ℤ) : (d.scale2 n).toRat = d.toRat * 2 ^ n

scale2 multiplies by 2^n

theorem LeanCert.Core.Dyadic.toRat_scale2_le_scale2 (d₁ d₂ : Dyadic) (n : ℤ) (h : d₁.toRat ≤ d₂.toRat) : (d₁.scale2 n).toRat ≤ (d₂.scale2 n).toRat

scale2 preserves order

Square Root Operations

def LeanCert.Core.Dyadic.intSqrtNat (n : ℕ) : ℕ

Integer square root of a natural number. Satisfies: (intSqrtNat n)^2 ≤ n < (intSqrtNat n + 1)^2

Equations

• LeanCert.Core.Dyadic.intSqrtNat n = n.sqrt

def LeanCert.Core.Dyadic.intSqrt (n : ℤ) : ℤ

Integer square root of a non-negative integer. Returns 0 for negative inputs.

Equations

• LeanCert.Core.Dyadic.intSqrt n = if n < 0 then 0 else Int.ofNat (LeanCert.Core.Dyadic.intSqrtNat n.toNat)

theorem LeanCert.Core.Dyadic.intSqrt_sq_le {n : ℤ} (hn : 0 ≤ n) : intSqrt n ^ 2 ≤ n

intSqrt n ^ 2 ≤ n for n ≥ 0

theorem LeanCert.Core.Dyadic.int_lt_succ_sqrt_sq {n : ℤ} (hn : 0 ≤ n) : n < (intSqrt n + 1) ^ 2

n < (intSqrt n + 1) ^ 2 for n ≥ 0

theorem LeanCert.Core.Dyadic.intSqrt_nonneg {n : ℤ} (hn : 0 ≤ n) : 0 ≤ intSqrt n

intSqrt is nonnegative for nonnegative inputs

def LeanCert.Core.Dyadic.sqrtDown (d : Dyadic) (prec : ℤ) : Dyadic

Compute sqrt(d) with a target exponent prec. Returns a Dyadic with exponent prec such that result ≤ sqrt(d).

For d = m * 2^e, we compute:

• shift = e - 2*prec (to align for sqrt)
• m' = m * 2^shift (or m / 2^(-shift) if shift < 0)
• result = floor(sqrt(m')) * 2^prec

This ensures: result.toRat ≤ sqrt(d.toRat)

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Core.Dyadic.sqrtUp (d : Dyadic) (prec : ℤ) : Dyadic

Compute sqrt(d) rounded up with target exponent prec. Returns a Dyadic with exponent prec such that result ≥ sqrt(d).

Uses the same computation as sqrtDown, but if the result is not a perfect square, adds 1 to round up.

Equations

• One or more equations did not get rendered due to their size.

Sqrt Correctness Theorems

theorem LeanCert.Core.Dyadic.sqrtDown_nonneg (d : Dyadic) (prec : ℤ) (hd : 0 ≤ d.mantissa) : 0 ≤ (d.sqrtDown prec).mantissa

sqrtDown is non-negative for non-negative inputs

theorem LeanCert.Core.Dyadic.sqrtUp_nonneg (d : Dyadic) (prec : ℤ) (hd : 0 ≤ d.mantissa) : 0 ≤ (d.sqrtUp prec).mantissa

sqrtUp is non-negative for non-negative inputs

theorem LeanCert.Core.Dyadic.sqrtDown_le_sqrtUp (d : Dyadic) (prec : ℤ) (hd : 0 ≤ d.mantissa) : (d.sqrtDown prec).toRat ≤ (d.sqrtUp prec).toRat

sqrtDown.toRat ≤ sqrtUp.toRat for non-negative inputs