spec: exact comparison of real algebraic numbers

[kim-em]

Objective

Specify exact sign determination and comparison of real algebraic numbers
thoroughly: every executable strategy, the theorem tying each to the
reference semantics, the input-computable termination bound of each, and the
Phase-4 evidence that decides which strategy runs where. The text lands in
SPEC/Libraries/hex-real-algebraic.md (the consumer) with the new primitives
specified in the SPECs of the libraries that own them (hex-real-roots for
Tarski queries, hex-number-field for lazy and fixed-field comparison).

Current state

• AlgebraicNumber.realCompare (HexNumberField/Nearest.lean) already
  rejects on disjoint stored intervals, then refines both operands on a
  geometric schedule capped at separationPrec (a.p * b.p) + 1, and only
  then falls back to realCompareExact, which approximates both numbers at
  the Mahler-bound precision of the product polynomial. realCompare_eq and
  realCompareExact_eq prove both return the real order. The SPEC documents
  this as the existing reference path rather than designing it again.
• Nothing compares two factorization-lazy AlgebraicRoots without
  exactifying both, which costs two Berlekamp–Zassenhaus factorizations.
• Nothing determines the sign of a fixed-field element f(α) : QAdjoin a
  without approximation, and nothing orders real elements of a
  NumberTower.
• hex-rcf builds and kernel-replays literal Sturm chains, but
  SturmReplay.check requires the second entry to be a positive multiple of
  the derivative, strictly descending degrees, and a terminal nonzero
  constant; its common-root packages replay the gcd's own derivative chain.
  It does not cover sturm(p, f·p') for arbitrary f, a zero f, or a
  nonconstant gcd. Its step 5 decides the position of a root relative to a
  dyadic endpoint by one Sturm count plus exact evaluation. Neither is
  exposed as a comparison primitive.
• Isolation precision separates the roots of a polynomial from each other,
  not from zero when zero is not a root. ofEliminant? isolates at
  separationDepth p, which is 12 for every linear polynomial whatever its
  height, so the lazy difference (±2⁻ᵏ) − 0 for k ≥ 13 is a nonzero root
  whose stored real centre is 0. The sign of the isolation centre therefore
  does not decide the order, and the previous text of this directive was
  wrong to say it did.
• No benchmark measures comparison at all.

Required design

• Reference semantics: realCompare remains the definition. Every fast path
  below is specified with a theorem that it returns the same Ordering.
• Stored-isolation fast path: realCompare as it exists, with its theorem
  and its structural fuel (the geometric schedule to the product-polynomial
  separation precision) stated in the SPEC; equality is decided structurally
  with no refinement. Any change to the schedule must preserve
  realCompare_eq.
• Comparison against a rational or dyadic point: the exact sign of the
  minimal polynomial at the point plus one Sturm count on the split interval
  (hex-rcf's endpoint test), no refinement, no factorization.
• Lazy comparison: AlgebraicRoot.compare as the sign of the difference,
  using the eliminant sub? already builds, then isZero, then a
  certified sign for the nonzero difference d with stored polynomial
  p (squarefree, primitive, positive leading coefficient):
  • degree one: the sign of −p.coeff 0;
  • degree at least two with p.coeff 0 ≠ 0: the stored centre has the
    exact sign, because separationDepth p ≥ ceilLog2 H + 12 for
    H = coeffAbsMax p while every nonzero root has
    |α| ≥ 1/(1 + H) ≥ 2^(−(ceilLog2 H + 1)) (reciprocal Cauchy) and the
    stored disc radius is below 2^(1 − prec);
  • degree at least two with p.coeff 0 = 0: zero is another root of p,
    so the root-separation guarantee of the isolation already excludes zero
    from the disc and the centre sign is exact.
    The companion proves this bound explicitly; it is not a remark. The SPEC
    states the invariant every lazy root relies on, that its stored precision
    is at least separationDepth of its stored polynomial, and either shows
    every AlgebraicRoot constructor maintains it or has compare refine to
    that depth first. If the SPEC prefers a uniform rule to the degree split,
    the alternative is one bounded refinement pass to the reciprocal-Cauchy
    depth of the difference eliminant (after removing its maximal X power)
    whenever the stored real interval meets zero, with that cost stated next to
    the resultant and the isolation. Say when either beats exactifying.
• Sign in a fixed field: for real α and f : QAdjoin a, (i) the Tarski
  query TaQ(f, p; I) from the Sturm chain of (p, f·p') evaluated at the
  dyadic endpoints of the isolating interval, exact integer arithmetic with
  no refinement, added to hex-real-roots as tarskiQuery and reusing
  hex-rcf's replay shape; (ii) approximation at the a priori precision from
  Disambiguation.evalMajorant and the reciprocal Cauchy bound. Specify
  both; the default per degree and height regime is left to Phase 4.
• Tower elements: the sign of a real NumberTower.Elem by fixed-embedding
  evaluation with the same majorant bound, and comparison inside a real
  tower.
• Sorting, min, max and Ord on arrays of real algebraic numbers, reusing
  the algebraicRoots order where the numbers share a polynomial.
• Certificates: state which comparisons are kernel-checkable (a Tarski query
  against dyadic endpoints is, since hex-rcf already replays Sturm chains in
  the kernel) and whether a decide-style comparison proof is worth
  exposing now or deferred.
• Phase-4 evidence per SPEC/benchmarking.md: families for well-separated
  pairs (degree sweep), close real pairs from Mignotte x^n − (a·x − 1)²
  (sweep in a), equal numbers from different lazy polynomials,
  rational-point comparisons, and fixed-field sign at growing coefficient
  height. Comparators: python-flint qqbar and Z3's RCF Python bindings,
  both informational; Sage AA is not an oracle. Required-check ceilings
  follow the existing mode rules.
• Conformance: python-flint supplies expected orderings; cypari2 cannot.

Do not implement in this issue.

Verification

• Each strategy has a stated equality theorem against realCompare and a
  stated input-computable termination bound.
• Confirm that hex-rcf's generalized replay covers sturm(p, f·p') for
  arbitrary f, or state the extension needed.
• Sanity-check every strategy on equal numbers, on numbers closer than the
  stored isolation width, on the sign of zero in a fixed field, on a
  rational point that is exactly a root, and on the lazy differences
  (±2⁻ᵏ) − 0 for k ∈ {20, 50, 100} and (a ± 2⁻ᵏ) − a for a
  quadratic irrational a, which must return the strict order.
• The lazy-comparison sign rule is stated with the theorem that justifies
  it; no strategy relies on the sign of an isolation centre without a stated
  lower bound on the value it approximates.
• All relative links resolve; git diff --check passes.

Dependencies

depends-on: #10141

[kim-em]

Claimed, but the premise check found a counterexample to the required lazy comparison strategy. Per the repository's “Directives are hypotheses, not specs” instruction, I am stopping before a SPEC PR and leaving this issue open for an updated directive.

The requested sequence “existing sub?, then isZero and the sign of the isolation centre” does not determine the order. Both +2⁻²⁰ - 0 and −2⁻²⁰ - 0 return a nonzero lazy root whose real isolation centre is zero. Thus even choosing either strict ordering when the centre is zero fails on one of the two inputs.

Reproducer (built with lake build ComparisonProbe, Lean 4.34.0, using matching existing library build artifacts):

import HexNumberField.Lazy
open Hex
set_option maxRecDepth 100000
set_option maxHeartbeats 0
#eval do
  for k in [20, 50, 100] do
    for sign in ([1, -1] : List Int) do
      let q : Rat := ((sign : Int) : Rat) / (2 ^ k : Rat)
      let raw : ZPoly := DensePoly.ofList [-sign, 2 ^ k]
      let some a := AlgebraicRoot.ofEliminant? raw
          (fun prec => some (DyadicComplexBall.ofRat q prec))
        | IO.println "input none"
      match a.sub? AlgebraicNumber.zero.toRoot with
      | none => IO.println "subtraction none"
      | some d =>
        IO.println s!"sign={sign}, k={k}: zero={d.isZero}, re={d.rep.1.square.re.toRat}, prec={d.rep.1.square.prec}"

All six cases succeed with zero=false, re=0, prec=13; the returned polynomial is [-sign, 2^k], whose unique real root is sign / 2^k.

Source explanation at cc2baf8:

• AlgebraicRoot.isZero tests p.coeff 0 == 0 && rep.containsZero. A negative zero test does not imply the disc excludes zero.
• ofEliminant? isolates at separationDepth p. That separates roots of p from each other, not from zero when zero is not a root.
• mahlerPrec is 3 for every linear polynomial, regardless of height, and separationDepth is 12. It therefore cannot resolve arbitrarily small nonzero linear roots from zero.

Suggested directive correction: retain the exact zero test, but require a certified sign decision for the nonzero difference. Probe its real-coordinate interval first; if it meets zero, use bounded refinement from a reciprocal-Cauchy lower bound for the nonzero roots of the difference eliminant (remove its maximal X power first). Alternatively, include zero as a root of the polynomial used for the separation bound. State this additional refinement cost alongside the resultant and isolation, and include the tiny positive/negative rational cases above among the sanity checks. Neither approach requires factorization, but the extra sign-separation step cannot be omitted.

A smaller amendment is possible: special-case a degree-one difference eliminant by returning the sign of -p.coeff 0 (the leading coefficient is positive). For degree at least two, prove that the existing stored precision already suffices for nonzero sign: writing H = coeffAbsMax p ≥ 1 and L = ceilLog2 H, the formula gives separationDepth p ≥ L + 12, while reciprocal Cauchy gives |α| ≥ 1/(1+H) ≥ 2^(-(L+1)) for any nonzero root. The stored disc radius is below 2^(1-prec), so the centre has the same strict sign. This amendment preserves the one-resultant/one-isolation cost without a new refinement pass, but changes the required centre-sign rule in the linear case. The companion must prove this lower-bound bridge explicitly.

Two other source observations for the revised specification:

• realCompare already implements stored-interval rejection and bounded geometric refinement; realCompareExact is the fixed-precision reference arm. The existing realCompare_eq and realCompareExact_eq theorems establish the same real order.
• RCF's SturmReplay.check requires p' = derivScale * s₁ with positive scale, strictly descending degrees, and a terminal nonzero constant. Common-root packages replay the gcd's derivative chain. This does not already cover arbitrary (p, f*p'), zero f, or a nonconstant gcd. The issue explicitly permits specifying the extension, so this is a design obligation rather than a second blocker.

No repository files were changed, no workaround sub-issue was filed, and no PR was opened.