theorem Hex.AlgebraicNumber.partialCompareExact_eq (a b : AlgebraicNumber) : a.partialCompareExact b = if a.toComplex.im = b.toComplex.im then some (compare a.toComplex.re b.toComplex.re) else none

Partial comparison detects exactly equal imaginary parts and compares real parts.

theorem Hex.AlgebraicNumber.apartProbe_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (v : Unit) (h : apartProbe (↑a).square (↑b).square = some v) : a.root.im ≠ b.root.im

Successful imaginary-interval probes reject equality.

theorem Hex.AlgebraicNumber.partialCompare_eq (a b : AlgebraicNumber) : a.partialCompare b = if a.toComplex.im = b.toComplex.im then some (compare a.toComplex.re b.toComplex.re) else none

The bounded partial comparator retains its exact semantics.

theorem Hex.AlgebraicNumber.ordered_exact (strict : Bool) (a b : AlgebraicNumber) : ordered strict (a.partialCompareExact b) = true ↔ (if strict = true then a.toComplex.re < b.toComplex.re else a.toComplex.re ≤ b.toComplex.re) ∧ a.toComplex.im = b.toComplex.im

Predicate extraction from the reference comparison.

theorem Hex.AlgebraicNumber.rejectProbe_sound (strict : Bool) {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (v : Unit) (h : rejectProbe strict (↑a).square (↑b).square = some v) : ¬((if strict = true then a.root.re < b.root.re else a.root.re ≤ b.root.re) ∧ a.root.im = b.root.im)

Rejection probes never reject a true complex comparison.

theorem Hex.AlgebraicNumber.orderBool_iff (strict : Bool) (a b : AlgebraicNumber) : orderBool strict a b = true ↔ (if strict = true then a.toComplex.re < b.toComplex.re else a.toComplex.re ≤ b.toComplex.re) ∧ a.toComplex.im = b.toComplex.im

Predicate-specific interval shortcuts preserve complex order.

theorem Hex.AlgebraicNumber.le_iff (a b : AlgebraicNumber) : a ≤ b ↔ a.toComplex.re ≤ b.toComplex.re ∧ a.toComplex.im = b.toComplex.im

The executable non-strict comparison has Mathlib's complex semantics.

theorem Hex.AlgebraicNumber.lt_iff (a b : AlgebraicNumber) : a < b ↔ a.toComplex.re < b.toComplex.re ∧ a.toComplex.im = b.toComplex.im

The executable strict comparison has Mathlib's complex semantics.

@[instance_reducible]

instance Hex.AlgebraicNumber.instPartialOrder_hexNumberFieldMathlib : PartialOrder AlgebraicNumber

Equations

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

instance Hex.AlgebraicNumber.instIsStrictOrderedRing_hexNumberFieldMathlib : IsStrictOrderedRing AlgebraicNumber

noncomputable def Hex.AlgebraicNumber.toComplexOrder : AlgebraicNumber ↪o ℂ

Interpretation is an embedding for the complex partial order.

Equations

• Hex.AlgebraicNumber.toComplexOrder = { toFun := Hex.AlgebraicNumber.toComplex, inj' := Hex.AlgebraicNumber.toComplex_injective, map_rel_iff' := @Hex.AlgebraicNumber.toComplexOrder._proof_1✝ }