theorem Hex.RootSelection.integerRoots?_eq (p : ZPoly) : p.algebraicRoots? = do let roots ← integerRoots? p let values ← Array.mapM AlgebraicRoot.exact? roots pure (values.toList.mergeSort AlgebraicNumber.rootLe).toArray

Exactifying the lazy isolations recovers the canonical integer-root computation.

theorem Hex.RootSelection.integerRoots?_isSome (p : ZPoly) : (integerRoots? p).isSome = true

Every integer polynomial has a successfully certified lazy root list.

theorem Hex.RootSelection.integerRoots?_mem (p : ZPoly) (hp : p ≠ 0) {roots : Array AlgebraicRoot} (h : integerRoots? p = some roots) (z : ℂ) : (∃ r ∈ roots.toList, r.toComplex = z) ↔ (HexRootsMathlib.toPolyℂ p).IsRoot z

The lazy list contains exactly the complex roots of a nonzero integer polynomial.