10.5. Squarefreeness is invisible🔗

Sturm isolation needs a squarefree polynomial, but the user never has to supply one. When the input has repeated roots the elaborator isolates its squarefree core and transports the certificate back to the original polynomial, so a polynomial like (x − 1)²(x − 3) isolates as its two distinct roots with no bookkeeping at the call site:

open Hex Polynomial

noncomputable def cubeRoots :
    IsolatedRealRoots
      ((X - 1) ^ 2 * (X - 3) : Polynomial ℝ) 2 :=
  isolate_roots ((X - 1) ^ 2 * (X - 3))

example : cubeRoots.intervals = #v[(0, 2), (2, 4)] :=
  rfl

A polynomial with no real roots isolates as the empty vector, and a nonzero constant isolates as n = 0 without ever entering the isolator. The zero polynomial is rejected, since every real number is a root.