Unnormalized dyadic numbers

⟨m, e⟩ : QI is m / 2^e. Operations never normalize: addition aligns exponents by a multiplication with 2^d (computed with Nat.pow, which the kernel evaluates with GMP), and comparison cross-multiplies. Every operation is a handful of Int/Nat primitives, which keeps decide +kernel evaluation cheap (core Dyadic normalizes with a well-founded loop).

structure Cayley.QI : Type

The dyadic number m / 2^e.

• m : Int
• e : Nat

@[instance_reducible]

instance Cayley.instInhabitedQI : Inhabited QI

Equations

• Cayley.instInhabitedQI = { default := Cayley.instInhabitedQI.default }

@[inline]

def Cayley.QI.pow2 (k : Nat) : Int

2^k as an integer.

Equations

• Cayley.QI.pow2 k = ↑(2 ^ k)

def Cayley.QI.add (a b : QI) : QI

Equations

• a.add b = if a.e ≤ b.e then { m := a.m * Cayley.QI.pow2 (b.e - a.e) + b.m, e := b.e } else { m := a.m + b.m * Cayley.QI.pow2 (a.e - b.e), e := a.e }

def Cayley.QI.mul (a b : QI) : QI

Equations

• a.mul b = { m := a.m * b.m, e := a.e + b.e }

def Cayley.QI.neg (a : QI) : QI

Equations

• a.neg = { m := -a.m, e := a.e }

def Cayley.QI.sub (a b : QI) : QI

Equations

• a.sub b = a.add b.neg

@[instance_reducible]

instance Cayley.QI.instAdd : Add QI

Equations

• Cayley.QI.instAdd = { add := Cayley.QI.add }

@[instance_reducible]

instance Cayley.QI.instMul : Mul QI

Equations

• Cayley.QI.instMul = { mul := Cayley.QI.mul }

@[instance_reducible]

instance Cayley.QI.instNeg : Neg QI

Equations

• Cayley.QI.instNeg = { neg := Cayley.QI.neg }

@[instance_reducible]

instance Cayley.QI.instSub : Sub QI

Equations

• Cayley.QI.instSub = { sub := Cayley.QI.sub }

@[instance_reducible]

instance Cayley.QI.instOfNat (n : Nat) : OfNat QI n

Equations

• Cayley.QI.instOfNat n = { ofNat := { m := ↑n, e := 0 } }

@[instance_reducible]

instance Cayley.QI.instIntCast : IntCast QI

Equations

• Cayley.QI.instIntCast = { intCast := fun (n : Int) => { m := n, e := 0 } }

@[instance_reducible]

instance Cayley.QI.instNatCast : NatCast QI

Equations

• Cayley.QI.instNatCast = { natCast := fun (n : Nat) => { m := ↑n, e := 0 } }

def Cayley.QI.le (a b : QI) : Prop

a ≤ b by cross-multiplication.

Equations

• a.le b = (a.m * Cayley.QI.pow2 b.e ≤ b.m * Cayley.QI.pow2 a.e)

def Cayley.QI.lt (a b : QI) : Prop

Equations

• a.lt b = (a.m * Cayley.QI.pow2 b.e < b.m * Cayley.QI.pow2 a.e)

@[instance_reducible]

instance Cayley.QI.instLE : LE QI

Equations

• Cayley.QI.instLE = { le := Cayley.QI.le }

@[instance_reducible]

instance Cayley.QI.instLT : LT QI

Equations

• Cayley.QI.instLT = { lt := Cayley.QI.lt }

@[instance_reducible]

instance Cayley.QI.instDecidableLe (a b : QI) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = Cayley.QI.instDecidableLe._aux_1 a b

@[instance_reducible]

instance Cayley.QI.instDecidableLt (a b : QI) : Decidable (a < b)

Equations

• a.instDecidableLt b = Cayley.QI.instDecidableLt._aux_1 a b