structure Hex.RCF.SturmStep : Type

One positive three-term recurrence in a generalized Sturm replay.

• leftScale : Int

  Positive scale on the polynomial two positions before the new term.

• quotient : ZPoly

  Quotient multiplying the preceding polynomial.

• rightScale : Int

  Positive scale on the new polynomial.

structure Hex.RCF.SturmReplay : Type

A literal generalized Sturm chain and its multiplication-only replay.

• chain : Array ZPoly

  The chain [f, s₁, …, sₙ].

• derivScale : Int

  Positive integer δ satisfying f' = δ s₁.

• steps : Array SturmStep

  The three-term identities for consecutive chain triples.

def Hex.RCF.SturmReplay.checkStep (a b c : ZPoly) (step : SturmStep) : Bool

Boolean validation of a supplied positive three-term identity.

Equations

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

def Hex.RCF.SturmReplay.checkSteps : ZPoly → ZPoly → List ZPoly → List SturmStep → Bool

Validate recurrence steps and the terminal nonzero constant.

Equations

• Hex.RCF.SturmReplay.checkSteps x✝¹ x✝ [] [] = decide (Hex.DensePoly.size x✝ = 1)
• Hex.RCF.SturmReplay.checkSteps x✝¹ x✝ (c :: rest) (step :: steps) = (Hex.RCF.SturmReplay.checkStep x✝¹ x✝ c step && Hex.RCF.SturmReplay.checkSteps x✝ c rest steps)
• Hex.RCF.SturmReplay.checkSteps x✝³ x✝² x✝¹ x✝ = false

def Hex.RCF.SturmReplay.checkNonzero : List ZPoly → Bool

Every literal polynomial in a chain is nonzero.

Equations

• Hex.RCF.SturmReplay.checkNonzero [] = true
• Hex.RCF.SturmReplay.checkNonzero (p :: rest) = (!Hex.DensePoly.isZero p && Hex.RCF.SturmReplay.checkNonzero rest)

def Hex.RCF.SturmReplay.checkDegrees : List ZPoly → Bool

Consecutive literal chain degrees strictly decrease.

Equations

• Hex.RCF.SturmReplay.checkDegrees (a :: b :: rest) = (decide (Hex.DensePoly.natDegree b < Hex.DensePoly.natDegree a) && Hex.RCF.SturmReplay.checkDegrees (b :: rest))
• Hex.RCF.SturmReplay.checkDegrees x✝ = true

def Hex.RCF.SturmReplay.check (f : ZPoly) (cert : SturmReplay) : Bool

Executable generalized Sturm replay checker.

All polynomial comparisons use DensePoly.beqCoeffs, avoiding structural array equality during kernel reduction. Nonzero checking before strict degree descent makes natDegree unambiguous and implies that an accepted head has positive degree. Degree descent is retained as an explicit certificate invariant even though the abstract IsSturmChain consequence does not need it.

Equations

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

def Hex.RCF.SturmReplay.count (cert : SturmReplay) (I : DyadicInterval) : Int

Literal Sturm variation drop across the dyadic interval (I.lower, I.upper].

Equations

• cert.count I = ↑(Hex.sturmVarAt cert.chain I.lower) - ↑(Hex.sturmVarAt cert.chain I.upper)

def Hex.RCF.SturmReplay.total (cert : SturmReplay) : Int

Literal Sturm variation drop from negative to positive infinity.

Equations

• cert.total = ↑(Hex.sturmVarNegInf cert.chain) - ↑(Hex.sturmVarPosInf cert.chain)

def Hex.RCF.SturmReplay.DegreesDescend : List ZPoly → Prop

Proposition-level adjacent degree descent mirrored by checkDegrees.

Equations

• Hex.RCF.SturmReplay.DegreesDescend (a :: b :: rest) = (Hex.DensePoly.natDegree b < Hex.DensePoly.natDegree a ∧ Hex.RCF.SturmReplay.DegreesDescend (b :: rest))
• Hex.RCF.SturmReplay.DegreesDescend x✝ = True

theorem Hex.RCF.SturmReplay.checkNonzero_sound {chain : List ZPoly} (h : checkNonzero chain = true) (q : ZPoly) : q ∈ chain → q ≠ 0

A successful nonzero walk proves every chain entry nonzero.

theorem Hex.RCF.SturmReplay.checkDegrees_sound {chain : List ZPoly} (h : checkDegrees chain = true) : DegreesDescend chain

A successful degree walk proves proposition-level adjacent descent.

theorem Hex.RCF.SturmReplay.head_ne_zero {f : ZPoly} {cert : SturmReplay} (h : check f cert = true) : f ≠ 0

The head of an accepted replay is nonzero.