Positive-scaled signed remainder chains

The defining relations allow pseudo-remainder scaling. The terminal entry may be nonconstant; no coprimality is imposed on the first two entries.

Polynomial.sturmSeq satisfies these relations. The relational formulation also allows positive pseudo-remainder scalings without changing root sign sums.

def TauCeti.Sturm.IsRemainder {R : Type u_1} [Field R] [LinearOrder R] (p q r : Polynomial R) : Prop

A positively scaled signed remainder identity.

Equations

• TauCeti.Sturm.IsRemainder p q r = ∃ (a : R) (b : R) (u : Polynomial R), 0 < a ∧ 0 < b ∧ Polynomial.C a * p = u * q - Polynomial.C b * r

structure TauCeti.Sturm.IsSignedRemainderSeq {R : Type u_1} [Field R] [LinearOrder R] (cs : List (Polynomial R)) : Prop

The algebraic relations of a signed remainder chain, including its exact termination. Degree descent is needed to construct such a chain, but not to verify its signed root-sum identity.

• nonzero (p : Polynomial R) : p ∈ cs → p ≠ 0

  Every entry is a nonzero polynomial.

• relation (i : ℕ) (p q r : Polynomial R) : cs[i]? = some p → cs[i + 1]? = some q → cs[i + 2]? = some r → IsRemainder p q r

  Successive triples satisfy a positively scaled signed remainder identity.

• terminal (pre : List (Polynomial R)) (p q : Polynomial R) : cs = pre ++ [p, q] → q ∣ p

  The final remainder vanishes, so the last entry divides its predecessor.

theorem TauCeti.Sturm.IsRemainder.of_identity {R : Type u_1} [Field R] [LinearOrder R] {p q r : Polynomial R} (a b : R) (u : Polynomial R) (ha : 0 < a) (hb : 0 < b) (heq : Polynomial.C a * p = u * q - Polynomial.C b * r) : IsRemainder p q r

Construct the signed remainder relation from positive scalings and a polynomial identity.

theorem TauCeti.Sturm.IsRemainder.exists_identity {R : Type u_1} [Field R] [LinearOrder R] {p q r : Polynomial R} (h : IsRemainder p q r) : ∃ (a : R) (b : R) (u : Polynomial R), 0 < a ∧ 0 < b ∧ Polynomial.C a * p = u * q - Polynomial.C b * r

A signed remainder relation supplies positive scalings and its polynomial identity.

theorem TauCeti.Sturm.IsRemainder.dvd {R : Type u_1} [Field R] [LinearOrder R] {p q r d : Polynomial R} (h : IsRemainder p q r) (hq : d ∣ q) (hr : d ∣ r) : d ∣ p

A common divisor of the two later entries divides the earlier entry.

theorem TauCeti.Sturm.IsRemainder.alternate {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p q r : Polynomial R} (h : IsRemainder p q r) {x : R} (hq : Polynomial.eval x q = 0) (hr : Polynomial.eval x r ≠ 0) : Polynomial.eval x p * Polynomial.eval x r < 0

At a zero of the middle entry, the neighbors have opposite signs, provided the right neighbor does not vanish.

theorem TauCeti.Sturm.IsSignedRemainderSeq.singleton {R : Type u_1} [Field R] [LinearOrder R] {p : Polynomial R} (hp : p ≠ 0) : IsSignedRemainderSeq [p]

A nonzero polynomial alone forms a signed remainder sequence.

theorem TauCeti.Sturm.IsSignedRemainderSeq.pair {R : Type u_1} [Field R] [LinearOrder R] {p q : Polynomial R} (hp : p ≠ 0) (hdvd : q ∣ p) : IsSignedRemainderSeq [p, q]

A two-entry chain terminates when its second polynomial divides its first.

theorem TauCeti.Sturm.IsSignedRemainderSeq.cons {R : Type u_1} [Field R] [LinearOrder R] {p q r : Polynomial R} {cs : List (Polynomial R)} (hp : p ≠ 0) (hrel : IsRemainder p q r) (h : IsSignedRemainderSeq (q :: r :: cs)) : IsSignedRemainderSeq (p :: q :: r :: cs)

Prepend one signed recurrence to a chain.

theorem TauCeti.Sturm.IsSignedRemainderSeq.tail {R : Type u_1} [Field R] [LinearOrder R] {p : Polynomial R} {cs : List (Polynomial R)} (h : IsSignedRemainderSeq (p :: cs)) : IsSignedRemainderSeq cs

theorem TauCeti.Sturm.IsSignedRemainderSeq.last_dvd {R : Type u_1} [Field R] [LinearOrder R] {cs : List (Polynomial R)} (h : IsSignedRemainderSeq cs) {d : Polynomial R} (hd : cs.getLast? = some d) (p : Polynomial R) : p ∈ cs → d ∣ p

The terminal polynomial divides every chain entry.

theorem TauCeti.Sturm.IsSignedRemainderSeq.isAlternating {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {cs : List (Polynomial R)} (h : IsSignedRemainderSeq cs) (hlast : ∀ (q : Polynomial R), cs.getLast? = some q → ∀ (x : R), Polynomial.eval x q ≠ 0) : IsAlternating cs

A signed remainder chain with a root-free last entry is alternating.

theorem TauCeti.Sturm.IsSignedRemainderSeq.sturmSeq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p q : Polynomial R) : IsSignedRemainderSeq (p.sturmSeq q)

Mathlib's signed remainder sequence satisfies the algebraic chain conditions.

theorem TauCeti.Sturm.IsRemainder.cancel {R : Type u_1} [Field R] [LinearOrder R] {d p q r : Polynomial R} (hd : d ≠ 0) (h : IsRemainder (d * p) (d * q) (d * r)) : IsRemainder p q r

Cancel a nonzero common polynomial factor from a signed remainder identity.

theorem TauCeti.Sturm.IsSignedRemainderSeq.cancel {R : Type u_1} [Field R] [LinearOrder R] {d : Polynomial R} {cs : List (Polynomial R)} (hd : d ≠ 0) (h : IsSignedRemainderSeq (List.map (fun (x : Polynomial R) => d * x) cs)) : IsSignedRemainderSeq cs

Dividing out a nonzero common factor preserves the signed chain conditions: if cs.map (d * ·) is signed, so is cs.

theorem TauCeti.Sturm.IsSignedRemainderSeq.exists_isAlternating {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {cs : List (Polynomial R)} (h : IsSignedRemainderSeq cs) {d : Polynomial R} (hd : cs.getLast? = some d) : ∃ (ds : List (Polynomial R)), cs = List.map (fun (x : Polynomial R) => d * x) ds ∧ ds.getLast? = some 1 ∧ IsSignedRemainderSeq ds ∧ IsAlternating ds

Divide every entry by the terminal common factor. The resulting chain is alternating and ends at 1, even when the original terminal factor is nonconstant.