def Hex.AlgebraicNumber.partialCompareExact (a b : AlgebraicNumber) : Option Ordering

Compare values on the same horizontal line; none means incomparable. Real inputs reuse realCompare, and differing half planes are rejected without arithmetic.

Equations

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

def Hex.AlgebraicNumber.apartProbe (a b : DyadicSquare) : Option Unit

A successful probe certifies unequal imaginary coordinates.

Equations

• Hex.AlgebraicNumber.apartProbe a b = if Hex.Interval.imagApart a b = true then some () else none

def Hex.AlgebraicNumber.partialCompare (a b : AlgebraicNumber) : Option Ordering

Partial comparison with bounded imaginary-interval rejection.

Equations

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

def Hex.AlgebraicNumber.rejectProbe (strict : Bool) (a b : DyadicSquare) : Option Unit

A successful probe rules out the requested complex-order predicate.

Equations

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

def Hex.AlgebraicNumber.ordered (strict : Bool) (result : Option Ordering) : Bool

Read a strict or non-strict predicate from a partial comparison.

Equations

• Hex.AlgebraicNumber.ordered strict result = Option.any (fun (o : Ordering) => if strict = true then o == Ordering.lt else o != Ordering.gt) result

def Hex.AlgebraicNumber.orderBool (strict : Bool) (a b : AlgebraicNumber) : Bool

Decide one predicate, rejecting impossible real inequalities without testing equality of imaginary coordinates. Neither a positive answer nor incomparability is guessed.

Equations

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

@[instance_reducible]

instance Hex.AlgebraicNumber.instLT : LT AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instLT = { lt := fun (a b : Hex.AlgebraicNumber) => Hex.AlgebraicNumber.orderBool true a b = true }

@[instance_reducible]

instance Hex.AlgebraicNumber.instLE : LE AlgebraicNumber

Equations

• Hex.AlgebraicNumber.instLE = { le := fun (a b : Hex.AlgebraicNumber) => Hex.AlgebraicNumber.orderBool false a b = true }

@[instance_reducible]

instance Hex.AlgebraicNumber.instDecidableLt (a b : AlgebraicNumber) : Decidable (a < b)

Equations

• a.instDecidableLt b = instDecidableEqBool (Hex.AlgebraicNumber.orderBool true a b) true

@[instance_reducible]

instance Hex.AlgebraicNumber.instDecidableLe (a b : AlgebraicNumber) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = instDecidableEqBool (Hex.AlgebraicNumber.orderBool false a b) true