29.8. Conjugation, order, and principal radicals🔗

Hex.AlgebraicNumber.conj is cheap: a nonreal number shares one canonical upper-half-plane isolation with its conjugate and stores a tag selecting the upper or lower value. Conjugation flips the tag. It does not factor a polynomial, isolate roots, refine a ball, or build an ever-growing certificate. Real values are unchanged. The companion provides StarRing and Hex.AlgebraicNumber.conjRingEquiv, with the usual arithmetic laws.

Root enumeration puts real roots first and nonreal conjugate pairs next to one another, the negative imaginary member first. Pairs use the upper isolation's dyadic centre (im, re, precision), with the minimal polynomial breaking remaining ties. This is a cheap deterministic enumeration order; it is not lexicographic comparison of exact complex coordinates. Root indices and nearest-root ties involving nonreal values may change when the isolation algorithm changes. A printed rootNear expression still names its original mathematical value. The companion proves sorting with Hex.ZPoly.algebraicRoots_sorted and the absence of intervening values with Hex.AlgebraicNumber.between_conjugates.

The global < and ≤ operations instead match Mathlib's complex partial order: imaginary parts must be equal, and real parts are compared. Thus I < 1 + I, while neither 0 ≤ I nor I ≤ 0. There is no total Ord or LinearOrder instance on algebraic numbers. Comparing unequal nonreal values on the same side of the real axis first tests stored coordinate intervals, then refines by 16 and 64 extra bits if needed. Disjoint imaginary intervals prove incomparability, and </≤ also reject impossible real inequalities. Real-real comparisons try stored intervals before computing a product separation bound and refining geometrically. Inconclusive complex comparisons compute an exact subtraction, so that fallback can cost as much as a field operation. Equal imaginary parts pay for inconclusive refinement before subtraction; the recorded same-imaginary benchmark was about 9% slower than the former comparison on the measured host. Use the real algebraic type for sorting real values by exact comparison. The companion's Hex.AlgebraicNumber.toComplexOrder preserves and reflects this order.

Hex.AlgebraicNumber.sqrt and Hex.AlgebraicNumber.nthRoot select Mathlib's principal complex branches. For a positive index n, the result has argument in (-π/n, π/n]. Index zero returns 1, including at zero. A negative real number's principal odd root is generally complex: nthRoot (-8) 3 is 1 + √3 I, not the real cube root -2.

The general implementation solves X^n - a with the existing algebraic coefficient solver. It filters lazy roots by their exact imaginary side, then selects maximal real part using certified intervals. It first checks stored intervals and tries two modest refinement rounds before falling back to exact coordinate comparisons. A successful interval selection exactifies only the winner. Overlap alone never establishes an ordering or equality. The general root solver and final canonicalization can still be expensive. Zero, one, and indices zero and one have direct paths; radicals of -1, I, and -I use the roots-of-unity constructor below.

Conjugation commutes with these branches away from the negative real axis; Hex.AlgebraicNumber.nthRoot_conj states the necessary argument hypothesis. The corollary Hex.AlgebraicNumber.nthRoot_conj_of_not_lt uses the executable condition ¬ a < 0, which holds exactly away from the negative real axis in the complex partial order. On the cut, both sqrt (-1) and sqrt (conj (-1)) are I, whereas conj (sqrt (-1)) is -I.