18.11. Arithmetic at a selected algebraic root🔗

HexRealClosure provides a computational interface for a selected real root of a rational polynomial, including a reducible one. The checked descriptor below selects √2 from (X² − 2)(X − 3) using the open interval (1, 2). The value a − 3 is nonzero at that root, even though it has a nonconstant gcd with the defining polynomial. Its checked inverse and the cofactor split use the selected root, not a quotient by the whole reducible polynomial.

The split creates context version 8 and explicitly refines a into it; the original a remains in context version 7. The checked d.handle caches the selected canonical root. Its pack method stores a representative with a unique zero. The resulting canonical value is positive and squares to 2. A polynomial over Root.Handle.Value h uses that same cached root for every coefficient operation, including division.

section
open Hex Hex.RealClosure

private def x : DensePoly Rat := DensePoly.ofCoeffs #[0, 1]
private def head : DensePoly Rat :=
  (DensePoly.ofCoeffs #[-2, 0, 1]) *
    (x - DensePoly.C 3)
private def raw : SignDet.RawDescriptor Rat Nat :=
  { context := 7, head, lower := .finite 1,
    upper := .finite 2,
    indices := [], signs := [] }

private def selectedArithmetic : Option
    (Int × Int × Int × Nat × Nat × Nat × Bool ×
      Bool × Bool) := do
  let d ← Root.validate 7 raw
  let a : Expression d := ⟨x⟩
  let below : Expression d := ⟨x - DensePoly.C 3⟩
  let inverse? ← below.inverse?.toOption
  let inverse ← inverse?
  let split? ←
    (below.split? 8 (.finite 1) (.finite 2)).toOption
  let split ← split?
  let oldSign ← a.sign?.toOption
  let newSign ← (Expression.refine split a).sign?.toOption
  let inverseSign ← inverse.sign?.toOption
  let h := d.handle
  let packed : Element d := h.pack x
  let selectedZero := h.pack (x * x - DensePoly.C 2)
  let v := h.value packed
  let coeff : Root.Handle.Value h :=
    Root.Handle.Value.ofPoly h x
  let y : DensePoly (Root.Handle.Value h) :=
    DensePoly.ofCoeffs #[0, 1]
  let (_, remainder) := DensePoly.divMod
    (y * y - DensePoly.C 2) (y - DensePoly.C coeff)
  return (oldSign, newSign, inverseSign,
    d.raw.context, split.binding.target.raw.context,
    split.binding.target.raw.head.natDegree,
    selectedZero == 0,
    v * v == Hex.RealAlgebraicNumber.ofRat 2 &&
      v.sign == 1,
    remainder.isZero)

#guard selectedArithmetic ==
  some (1, 1, -1, 7, 8, 2, true, true, true)
end

The companion proves that checked signs, inversion, refinement and canonical conversion preserve the selected real value. Those proofs use the shared accepted-query soundness theorem HexRealRootsTheory.Tarski.check_rootSum. Root.Handle.Value h carries the same packed representation and gives generic DensePoly algorithms operations that share this cached root. See HexNumberField for fixed-field arithmetic and HexRealAlgebraic for the canonical value API.