10.4. Requesting tighter intervals🔗

The natural intervals are only as tight as the isolator needed to separate the roots. Passing (width := x) refines every interval to width at most x, still with exact rational endpoints. The width may be written as a fraction, a power of two, or a decimal power: 1/1000, 2^(-20), 10^(-2) all work. Refining x⁴ − 2 to width 2⁻²⁰ places the positive root in an interval of width exactly 2⁻²⁰:

open Hex Polynomial

/-- The same two roots, isolated to width `2⁻²⁰`. -/
noncomputable def x4rootsTight :
    IsolatedRealRoots (X ^ 4 - 2 : Polynomial ℝ) 2 :=
  isolate_roots (width := 2 ^ (-20 : ℤ)) (X ^ 4 - 2)

/-- One real root in `(623487/2¹⁹, 1246975/2²⁰]`. -/
theorem root_pos_tight :
    ∃! x : ℝ, x ^ 4 - 2 = 0 ∧
      (623487 : ℝ) / 2 ^ 19 < x ∧ x ≤ 1246975 / 2 ^ 20 := by⊢ ∃! x, x ^ 4 - 2 = 0 ∧ 623487 / 2 ^ 19 < x ∧ x ≤ 1246975 / 2 ^ 20
  simpa [x4rootsTight] using x4rootsTight.unique_root 1All goals completed! 🐙

Width is an operational promise about the intervals the elaborator emits, not a field of the structure. Reading the refined endpoints back is still rfl, exactly as for the natural intervals; the refinement does not push Rat normalization into the kernel.