def Hex.signVar (l : List Int) : Nat

Zero-skipping sign variations of a list of exact integer values.

Drop the zero entries, then count the adjacent pairs of opposite sign (the product is negative). The variation count of (+, 0, −) is 1: the zero is skipped, leaving one sign change. This is the plain-List Int primitive shared by the Sturm counts below and the Descartes count in the Mobius layer.

Equations

• Hex.signVar l = Hex.signVar.go (List.filter (fun (x : Int) => x != 0) l)

def Hex.signVar.go : List Int → Nat

Count adjacent opposite-sign pairs of an already zero-free list.

Equations

• Hex.signVar.go (a :: b :: rest) = (if a * b < 0 then 1 else 0) + Hex.signVar.go (b :: rest)
• Hex.signVar.go a✝ = 0

def Hex.sturmVarAt (chain : Array ZPoly) (x : Dyadic) : Nat

Zero-skipping sign variations of the Sturm chain evaluated at a dyadic point x.

Every chain element is evaluated at x by exact Horner arithmetic (evalDyadic), reduced to its exact sign in {−1, 0, 1} (dyadicSign), and the resulting sign list is fed to signVar. No rounding and no error budget: the sign of q(x) at a dyadic x is exact.

Equations

• Hex.sturmVarAt chain x = Hex.signVar (List.map (fun (q : Hex.ZPoly) => Hex.dyadicSign (q.evalDyadic x)) chain.toList)

def Hex.sturmVarPosInf (chain : Array ZPoly) : Nat

Zero-skipping sign variations of the Sturm chain at +∞.

At +∞ the sign of each element is the sign of its leading coefficient, so no evaluation is needed. The zero polynomial has leading coefficient 0, which the zero-skipping convention drops (it never occurs in a genuine chain element, but the total function tolerates it).

Equations

• Hex.sturmVarPosInf chain = Hex.signVar (List.map (fun (q : Hex.ZPoly) => (Hex.DensePoly.leadingCoeff q).sign) chain.toList)

def Hex.sturmVarNegInf (chain : Array ZPoly) : Nat

Zero-skipping sign variations of the Sturm chain at −∞.

At −∞ the sign of each element is the sign of its leading coefficient times (−1)^{deg}: the leading term dominates, and its sign flips with the parity of the degree. No evaluation is needed. The zero polynomial has leading coefficient 0, dropped by the zero-skipping convention.

Equations

• Hex.sturmVarNegInf chain = Hex.signVar (List.map (fun (q : Hex.ZPoly) => (Hex.DensePoly.leadingCoeff q).sign * if Hex.DensePoly.natDegree q % 2 = 1 then -1 else 1) chain.toList)

def Hex.ZPoly.sturmCount (p : ZPoly) (I : DyadicInterval) : Int

The number of real roots of p in the half-open interval (I.lower, I.upper], as certified by the Sturm chain: the sign-variation difference between the two endpoints. An Int by definition. The companion proves it equals the root count in the interval (in particular, that it is nonnegative) for squarefree p.

Equations

• p.sturmCount I = ↑(Hex.sturmVarAt p.sturmChain I.lower) - ↑(Hex.sturmVarAt p.sturmChain I.upper)

def Hex.ZPoly.rootCount (p : ZPoly) : Nat

The total number of real roots of p: the sign-variation difference of its Sturm chain between −∞ and +∞.

Equations

• p.rootCount = Hex.sturmVarNegInf p.sturmChain - Hex.sturmVarPosInf p.sturmChain

structure Hex.RealRootIsolation (p : ZPoly) : Type

Exactly one real root of p lies in the half-open interval (interval.lower, interval.upper], witnessed by a Sturm count of 1. The witness is decidable data, dischargeable by decide.

• interval : DyadicInterval

  The half-open interval (lower, upper] containing the root.

• count_one : p.sturmCount self.interval = 1

  The Sturm count certifies exactly one root in the interval.

structure Hex.RealRootIsolations (p : ZPoly) : Type

A complete isolation run for p: pairwise-disjoint isolations, in increasing order, one per real root of p.

ordered records that the isolations are sorted with non-overlapping half-open intervals — the upper endpoint of each is at most the lower endpoint of the next. Because the intervals are half-open on the left, touching at a shared endpoint still leaves them disjoint as sets, so ordered gives pairwise disjointness for free. complete records that there are exactly ZPoly.rootCount p of them.

Both invariants are decidable data, so for squarefree p the structure certifies itself no matter which engine produced it: count_one puts exactly one root in each interval, ordered makes the intervals disjoint, and complete matches their number to the total root count, so every real root is captured exactly once.

• isolations : Array (RealRootIsolation p)

  The isolations, emitted in increasing order.

• ordered (i j : Fin self.isolations.size) : i < j → self.isolations[i].interval.upper ≤ self.isolations[j].interval.lower

  The half-open intervals are sorted and non-overlapping.

• complete : self.isolations.size = p.rootCount

  There is exactly one isolation per real root of p.

def Hex.assemble? (p : ZPoly) (chain : Array ZPoly) (hchain : chain = p.sturmChain) (arr : Array (RealRootIsolation p)) : Option (RealRootIsolations p)

Final-assembly helper shared by both isolation engines.

An engine emits its isolations in increasing order (a left-first DFS over the bisection tree), so there is no sorting to do here: assemble? only checks the two RealRootIsolations invariants and packages them. ordered is checked directly over arr; complete is checked against sturmVarNegInf chain − sturmVarPosInf chain on the caller's already-computed chain, and the hchain : chain = sturmChain p equality (passed as rfl by a caller whose chain is let-bound to sturmChain p) identifies that difference with ZPoly.rootCount p without recomputing the chain — the memoisation discipline of computing the chain once per polynomial.

A none here means the engine's output violated its own invariants; the drivers surface it as engine failure.

Equations

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