def Hex.ZPoly.isolateDescartes? (p : ZPoly) : Option (RealRootIsolations p)

The Descartes isolation engine.

ZPoly.isolateDescartes? classifies its input exactly as ZPoly.isolateSturm? does:

• p = 0 (degree? = none): none.

• p a nonzero constant (degree? = some 0): some with an empty isolation array, matching ZPoly.rootCount p = 0. assemble? certifies completeness (the chain is empty, so sturmVarNegInf − sturmVarPosInf = 0).

• p of positive degree that is not SquareFreeRat: none. Callers use Hex.ZPoly.squareFreeCore to obtain a square-free representative first.

• p of positive degree and square-free: build the chain once, run descartesVisit over (−rootBound p, rootBound p] with the depth budget isolationDepth p, then hand the ordered emissions to assemble?.

The engine trusts Descartes' rule for nothing; it is a search heuristic wrapped in Sturm certificates. A none on square-free positive-degree input means a candidate's Sturm count was not 1, an interval bisected past the depth budget, or the emitted total disagreed with ZPoly.rootCount p. The deferred companion theorem isolateDescartes?_isSome (the Obreshkoff two-circle theorem) says none of them happen for square-free input at this budget, so the driver's completeness — established through the Sturm engine — never waits on it. The per-node cost is one O(n²) Möbius transform against the Sturm engine's full chain evaluation, which is why this engine runs first in ZPoly.isolateRealRoots?.

Equations

• One or more equations did not get rendered due to their size.