@[reducible, inline]

abbrev Hex.ZPoly.beqCoeffs (a b : ZPoly) : Bool

Coefficient-level Boolean equality for ZPoly: the generic DensePoly.beqCoeffs at R = Int. Kept as an abbrev so the Sturm-chain checkers below read at the ZPoly level; see DensePoly.beqCoeffs for why this is used instead of the structural DecidableEq.

Equations

• a.beqCoeffs b = Hex.DensePoly.beqCoeffs a b

theorem Hex.ZPoly.eq_of_beqCoeffs {a b : ZPoly} (h : a.beqCoeffs b = true) : a = b

beqCoeffs is sound: a true result forces genuine polynomial equality.

def Hex.ZPoly.certTail : ZPoly → ZPoly → List ZPoly → Bool

The tail validator for SturmChainCert: given the two most recent chain elements prev, cur, check that rest continues the Sturm chain exactly as sturmChainAux builds it. An empty tail requires the next pseudo-remainder to vanish (sturmChainAux's stopping condition); a nonempty tail requires the pseudo-remainder nonzero, its next element = −primitivePart (spem prev cur), and the rest to continue from cur, next. Mirrors sturmChainAux's branch structure so certTail_sound is a direct induction.

Equations

• x✝¹.certTail x✝ [] = Hex.DensePoly.isZero (x✝¹.spem x✝)
• x✝¹.certTail x✝ (next :: rest) = (!Hex.DensePoly.isZero (x✝¹.spem x✝) && next.beqCoeffs (-(x✝¹.spem x✝).primitivePart) && x✝.certTail next rest)

theorem Hex.ZPoly.certTail_sound (fuel : Nat) (prev cur : ZPoly) (rest : List ZPoly) (acc : Array ZPoly) : prev.certTail cur rest = true → rest.length < fuel → (sturmChainAux fuel prev cur acc).toList = acc.toList ++ rest

The tail validator reconstructs sturmChainAux exactly: if certTail prev cur rest holds and there is enough fuel, then running sturmChainAux from prev, cur with accumulator acc yields acc followed by rest. Induction on rest.

def Hex.ZPoly.sturmChainCertB (p : ZPoly) (chain : Array ZPoly) : Bool

A decidable executable certificate that chain is the Sturm chain of p, by coefficient-level checks that kernel-reduce.

chain must have at least two elements, p must have positive degree (2 ≤ p.size) and chain must be no longer than p.size (a fuel bound that every genuine chain satisfies, since chain degrees strictly decrease). The head must be primitivePart p, the second primitivePart p', each further element −primitivePart (spem …) of its two predecessors, and the chain must terminate with a vanishing pseudo-remainder — exactly sturmChain's construction. All element comparisons go through beqCoeffs, never structural Array equality.

Equations

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

def Hex.SturmChainCert (p : ZPoly) (chain : Array ZPoly) : Prop

Chain-validity certificate: chain is the Sturm chain of p. A decidable Prop (the Bool-check = true pattern) verified by coefficient-level checks that kernel-reduce.

Equations

• Hex.SturmChainCert p chain = (p.sturmChainCertB chain = true)

@[instance_reducible]

instance Hex.instDecidableSturmChainCert (p : ZPoly) (chain : Array ZPoly) : Decidable (SturmChainCert p chain)

Equations

• Hex.instDecidableSturmChainCert p chain = Hex.instDecidableSturmChainCert._aux_1 p chain

theorem Hex.ZPoly.cert_imp_eq {p : ZPoly} {chain : Array ZPoly} (h : SturmChainCert p chain) : chain = p.sturmChain

Certificate soundness. A valid SturmChainCert p chain identifies chain with sturmChain p as a proposition. Proving (not deciding) this equality sidesteps the kernel Array.instDecidableEqImpl block.

theorem Hex.ZPoly.sturmCount_eq_of_cert {p : ZPoly} {chain : Array ZPoly} (h : SturmChainCert p chain) (I : DyadicInterval) : p.sturmCount I = ↑(sturmVarAt chain I.lower) - ↑(sturmVarAt chain I.upper)

Count transport. Under a valid certificate, the Sturm count of p on any interval is the sign-variation gap of the literal certified chain at the two endpoints — the shape the elaborator decides per emitted root.

theorem Hex.ZPoly.rootCount_eq_of_cert {p : ZPoly} {chain : Array ZPoly} (h : SturmChainCert p chain) : p.rootCount = sturmVarNegInf chain - sturmVarPosInf chain

Root-count transport. Under a valid certificate, the total root count of p is the −∞/+∞ sign-variation gap of the literal certified chain — the shape the elaborator decides for the complete field.

def Hex.orderedAdjacent {p : ZPoly} (arr : Array (RealRootIsolation p)) : Bool

An O(n) adjacent-pair order check on an emitted isolation array: every consecutive pair has upperᵢ ≤ lowerᵢ₊₁. The elaborator decides this in place of the quadratic RealRootIsolations.ordered, which ordered_of_adjacent recovers by transitivity.

Equations

• Hex.orderedAdjacent arr = (List.range (arr.size - 1)).all fun (i : Nat) => if h : i + 1 < arr.size then decide (arr[i].interval.upper ≤ arr[i + 1].interval.lower) else true

theorem Hex.adjacent_step {p : ZPoly} {arr : Array (RealRootIsolation p)} (h : orderedAdjacent arr = true) (i : Nat) (hi : i + 1 < arr.size) : arr[i].interval.upper ≤ arr[i + 1].interval.lower

Each adjacent inequality certified by orderedAdjacent.

theorem Hex.ordered_of_adjacent {p : ZPoly} {arr : Array (RealRootIsolation p)} (h : orderedAdjacent arr = true) (i j : Fin arr.size) : i < j → arr[i].interval.upper ≤ arr[j].interval.lower

The transitivity walk: orderedAdjacent (adjacent pairs) upgrades to the all-pairs RealRootIsolations.ordered shape, using each interval's own lower < upper to bridge consecutive gaps.