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

The Sturm isolation engine.

ZPoly.isolateSturm? classifies its input explicitly:

• 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 sturmVisit over (−rootBound p, rootBound p] with the depth budget isolationDepth p and the two initial memoised endpoint counts, then hand the ordered emissions to assemble?.

A none from this engine on square-free positive-degree input has one precise meaning: an interval at separation depth still reported two or more roots, or the emitted total disagreed with ZPoly.rootCount p. The companion proves both impossible for square-free input (isolateSturm?_isSome), so on that input the engine is total in the sense that matters.

Equations

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