def Sturm.ReplayStep (a b c : Polynomial ℝ) : Prop

A positive three-term Sturm recurrence C left * a = quotient * b - C right * c.

Equations

• Sturm.ReplayStep a b c = ∃ (left : ℝ) (quotient : Polynomial ℝ) (right : ℝ), 0 < left ∧ 0 < right ∧ Polynomial.C left * a = quotient * b - Polynomial.C right * c

inductive Sturm.Replay : Polynomial ℝ → Polynomial ℝ → List (Polynomial ℝ) → Prop

Recurrences for a chain of length at least two, ending in a unit.

The recursive shape is convenient both for a compiled array checker to build and for the soundness proof to consume: each constructor adds exactly one supplied three-term identity.

• pair {a b : Polynomial ℝ} (last : IsUnit b) : Replay a b []
• cons {a b c : Polynomial ℝ} {rest : List (Polynomial ℝ)} (step : ReplayStep a b c) (tail : Replay b c rest) : Replay a b (c :: rest)

theorem Sturm.Replay.first_coprime {a b : Polynomial ℝ} {rest : List (Polynomial ℝ)} (h : Replay a b rest) : IsCoprime a b

The first two entries of a replay are coprime.

theorem Sturm.Replay.pair_coprime {x y : Polynomial ℝ} {rest : List (Polynomial ℝ)} (h : Replay x y rest) (i : ℕ) (a b : Polynomial ℝ) : (x :: y :: rest)[i]? = some a → (x :: y :: rest)[i + 1]? = some b → IsCoprime a b

Every consecutive pair in a replay is coprime.

theorem Sturm.Replay.triple {x y : Polynomial ℝ} {rest : List (Polynomial ℝ)} (h : Replay x y rest) (i : ℕ) (a b c : Polynomial ℝ) : (x :: y :: rest)[i]? = some a → (x :: y :: rest)[i + 1]? = some b → (x :: y :: rest)[i + 2]? = some c → ReplayStep a b c

Every consecutive triple in a replay has its supplied positive recurrence.

theorem Sturm.Replay.last_unit {x y : Polynomial ℝ} {rest : List (Polynomial ℝ)} (h : Replay x y rest) (q : Polynomial ℝ) : (x :: y :: rest).getLast? = some q → IsUnit q

The last entry of a replay is a unit.

theorem Sturm.isChain_of_replay {f s₁ : Polynomial ℝ} {rest : List (Polynomial ℝ)} (hrep : Replay f s₁ rest) (hnz : ∀ q ∈ f :: s₁ :: rest, q ≠ 0) (δ : ℝ) (hδ : 0 < δ) (hderiv : Polynomial.derivative f = Polynomial.C δ * s₁) : IsSturmChain f (f :: s₁ :: rest)

A literal positive recurrence replay gives all generalized Sturm-chain axioms. Nonvanishing is kept explicit because a unit terminal and recurrence identities alone permit a zero entry immediately before a unit.

theorem Sturm.squarefree_of_replay {f s₁ : Polynomial ℝ} {rest : List (Polynomial ℝ)} (hrep : Replay f s₁ rest) (δ : ℝ) (hδ : 0 < δ) (hderiv : Polynomial.derivative f = Polynomial.C δ * s₁) : Squarefree f

A literal positive recurrence replay proves squarefreeness by genuine polynomial coprimality of the head and its derivative.

def HexRealRootsMathlib.ZReplayStep (a b c : Hex.ZPoly) : Prop

An integer-polynomial instance of a positive three-term recurrence.

Equations

• HexRealRootsMathlib.ZReplayStep a b c = ∃ (left : ℤ) (quotient : Hex.ZPoly) (right : ℤ), 0 < left ∧ 0 < right ∧ Hex.DensePoly.scale left a = quotient * b - Hex.DensePoly.scale right c

inductive HexRealRootsMathlib.ZReplay : Hex.ZPoly → Hex.ZPoly → List Hex.ZPoly → Prop

A literal integer-polynomial recurrence chain ending in a nonzero constant.

• pair {a b : Hex.ZPoly} (last : Hex.DensePoly.size b = 1) : ZReplay a b []
• cons {a b c : Hex.ZPoly} {rest : List Hex.ZPoly} (step : ZReplayStep a b c) (tail : ZReplay b c rest) : ZReplay a b (c :: rest)

theorem HexRealRootsMathlib.ZReplay.toReplay {a b : Hex.ZPoly} {rest : List Hex.ZPoly} (h : ZReplay a b rest) : Sturm.Replay (toPolyℝ a) (toPolyℝ b) (List.map toPolyℝ rest)

Cast a literal integer replay to the abstract real-polynomial replay.

theorem HexRealRootsMathlib.ZReplay.isChain {f s₁ : Hex.ZPoly} {rest : List Hex.ZPoly} (hrep : ZReplay f s₁ rest) (hnz : ∀ q ∈ f :: s₁ :: rest, q ≠ 0) (δ : ℤ) (hδ : 0 < δ) (hderiv : Hex.DensePoly.derivative f = Hex.DensePoly.scale δ s₁) : Sturm.IsSturmChain (toPolyℝ f) (List.map toPolyℝ (f :: s₁ :: rest))

Checked literal integer identities imply a generalized Sturm chain for the real cast.

theorem HexRealRootsMathlib.ZReplay.squarefree {f s₁ : Hex.ZPoly} {rest : List Hex.ZPoly} (hrep : ZReplay f s₁ rest) (δ : ℤ) (hδ : 0 < δ) (hderiv : Hex.DensePoly.derivative f = Hex.DensePoly.scale δ s₁) : Squarefree (toPolyℝ f)

Checked literal integer identities prove squarefreeness of the real cast.

def HexRealRootsMathlib.Literal.InInterval (I : Hex.DyadicInterval) (x : ℝ) : Prop

Membership in the real half-open interval represented by I.

Equations

• HexRealRootsMathlib.Literal.InInterval I x = (HexRealRootsMathlib.Dyadic.toReal I.lower < x ∧ x ≤ HexRealRootsMathlib.Dyadic.toReal I.upper)

noncomputable def HexRealRootsMathlib.Literal.rootsIn (f : Polynomial ℝ) (I : Hex.DyadicInterval) : Multiset ℝ

The multiset of real roots of f in a half-open dyadic interval.

Equations

• HexRealRootsMathlib.Literal.rootsIn f I = Multiset.filter (HexRealRootsMathlib.Literal.InInterval I) f.roots

theorem HexRealRootsMathlib.literalCount_eq_card_roots (p : Hex.ZPoly) (chain : Array Hex.ZPoly) (hsf : Squarefree (toPolyℝ p)) (hchain : Sturm.IsSturmChain (toPolyℝ p) (List.map toPolyℝ chain.toList)) (I : Hex.DyadicInterval) : ↑(Hex.sturmVarAt chain I.lower) - ↑(Hex.sturmVarAt chain I.upper) = ↑(Literal.rootsIn (toPolyℝ p) I).card

A literal chain's finite variation drop is the exact number of roots in a half-open dyadic interval. This reads the supplied chain directly and never calls the executable chain builder.

theorem HexRealRootsMathlib.literalRootCount_eq_card_roots (p : Hex.ZPoly) (chain : Array Hex.ZPoly) (hsf : Squarefree (toPolyℝ p)) (hchain : Sturm.IsSturmChain (toPolyℝ p) (List.map toPolyℝ chain.toList)) : ↑(Hex.sturmVarNegInf chain) - ↑(Hex.sturmVarPosInf chain) = ↑(toPolyℝ p).roots.card

A literal chain's variation drop at infinity is the exact total number of real roots.

theorem HexRealRootsMathlib.ZReplay.count_eq_card_roots {f s₁ : Hex.ZPoly} {rest : List Hex.ZPoly} (hrep : ZReplay f s₁ rest) (hnz : ∀ q ∈ f :: s₁ :: rest, q ≠ 0) (δ : ℤ) (hδ : 0 < δ) (hderiv : Hex.DensePoly.derivative f = Hex.DensePoly.scale δ s₁) (I : Hex.DyadicInterval) : ↑(Hex.sturmVarAt (f :: s₁ :: rest).toArray I.lower) - ↑(Hex.sturmVarAt (f :: s₁ :: rest).toArray I.upper) = ↑(Literal.rootsIn (toPolyℝ f) I).card

A checked integer replay gives the exact literal count on an interval.

The array consumed by the executable variation reader is the array conversion of the replay list, so no separate list/array alignment proof is required.

theorem HexRealRootsMathlib.ZReplay.total_eq_card_roots {f s₁ : Hex.ZPoly} {rest : List Hex.ZPoly} (hrep : ZReplay f s₁ rest) (hnz : ∀ q ∈ f :: s₁ :: rest, q ≠ 0) (δ : ℤ) (hδ : 0 < δ) (hderiv : Hex.DensePoly.derivative f = Hex.DensePoly.scale δ s₁) : ↑(Hex.sturmVarNegInf (f :: s₁ :: rest).toArray) - ↑(Hex.sturmVarPosInf (f :: s₁ :: rest).toArray) = ↑(toPolyℝ f).roots.card

A checked integer replay gives the exact total literal root count.