hex

13.3. The isolate_roots elaborator🔗

isolate_roots p takes a polynomial p and elaborates to a value of type Hex.IsolatedRealRoots. The polynomial may be a Polynomial ℤ, Polynomial ℚ, or Polynomial ℝ with integer coefficients, or a raw Hex.ZPoly (the Mathlib-free dense integer polynomial). The result structure carries the intervals and the three theorems that make them a genuine isolation.

🔗structure
Hex.IsolatedRealRoots.{u_1} {R : Type u_1} [CommRing R] [Algebra R ℝ]
  (P : Polynomial R) (n : ℕ) : Type
Hex.IsolatedRealRoots.{u_1} {R : Type u_1}
  [CommRing R] [Algebra R ℝ]
  (P : Polynomial R) (n : ℕ) : Type

A complete, certified real-root isolation of P : Polynomial R over ℝ: n rational intervals, each holding exactly one real root, together covering every real root, sorted and pairwise disjoint. Props are in aeval form so the same structure serves R = ℤ (a Hex.ZPoly via HexPolyZMathlib.toPolynomial), R = ℚ, and R = ℝ.

Constructor

Hex.IsolatedRealRoots.mk.{u_1}

Fields

intervals : Vector (ℚ × ℚ) n

The n isolating intervals (lower, upper], as pairs of rationals.

unique_root : ∀ (i : Fin n), ∃! x, (Polynomial.aeval x) P = 0 ∧ ↑self.intervals[i].1 < x ∧ x ≤ ↑self.intervals[i].2

Each interval holds exactly one real root of P.

covers : ∀ (x : ℝ), (Polynomial.aeval x) P = 0 → ∃ i, ↑self.intervals[i].1 < x ∧ x ≤ ↑self.intervals[i].2

Every real root of P lies in one of the intervals.

ordered : ∀ (i j : Fin n), i < j → self.intervals[i].2 ≤ self.intervals[j].1

The intervals are sorted and pairwise disjoint: the upper endpoint of each is at most the lower endpoint of every later one. With half-open intervals this makes n exactly the number of distinct real roots.

Take x⁴ − 2, whose two real roots are ±2^{1/4} ≈ ±1.189. One call isolates them. When the expected type is given — here through the definition's type ascription — it pins the coefficient ring, so the argument itself needs no annotation, and the type records the certified count 2:

open Hex Polynomial /-- Both real roots of `x⁴ − 2`, certified. -/ noncomputable def x4roots : IsolatedRealRoots (X ^ 4 - 2 : Polynomial ℝ) 2 := isolate_roots (X ^ 4 - 2)

The intervals field is an ordinary literal vector, so reading it back is definitional. With no width request the intervals are whatever the isolator's separation produced; here (-4, 0] and (0, 4]:

open Hex Polynomial example : x4roots.intervals = #v[(-4, 0), (0, 4)] := rfl