13.5. 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 must be a closed, strictly positive rational expression; a free variable, zero, or a negative value is rejected during elaboration. It may be written as a fraction, a power of two, or a decimal power: 1/1000, 2 ^ (-20 : ℤ), and 10 ^ (-2 : ℤ) all work.

Internally the elaborator chooses the least nonnegative k with 2⁻ᵏ ≤ x and refines to that binary target. Widths above one therefore request k = 0, which still refines any wider natural interval to width at most one; refinement only narrows, so a coarse request cannot undo the isolator's separation. A non-dyadic request can produce a strictly narrower interval than requested. 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.