Pseudo-Division

This file defines pseudo-division of multivariate polynomials, a fundamental operation in the Characteristic Set Method.

Main Definitions

• MvPolynomial.pseudoOf: Pseudo-division of g by f with respect to a variable i (over commutative rings).
• MvPolynomial.pseudo: General pseudo-division that handles constants and zero (over fields).
• MvPolynomial.setPseudo: Successive pseudo-division by all polynomials in a triangular set.
• MvPolynomial.setPseudoRem: Computes only the remainder (more efficient when quotients are not needed).
• MvPolynomial.isRemainder: A predicate stating that r is a valid remainder of g by f, meaning r is reduced w.r.t. f and init(f)^s * g = q * f + r for some s, q.
• MvPolynomial.isSetRemainder: A predicate stating that r is a valid remainder of g by a triangular set S, meaning r is reduced w.r.t. S and satisfies the extended division equation.

Main results

• pseudoOf_equation: init(f) ^ s * g = q * f + r where deg(r) < deg(f)
• pseudoOf_remainder_reducedTo: The remainder is reduced w.r.t. the divisor
• pseudo_remainder_isRemainder: The remainder satisfies the isRemainder predicate
• setPseudo_remainder_isSetRemainder: The remainder satisfies the isSetRemainder predicate
• setPseudo_remainder_eq_zero_of_mem: Elements of S have zero remainder when divided by S

References

• [Wen-Tsun Wu, Mathematics Mechanization][wen2000mathematics]

structure MvPolynomial.PseudoResult (α : Type u_1) : Type u_1

The result of a pseudo-division of g by f, satisfying the equation init(f) ^ s * g = q * f + r.

• exponent : ℕ

  The power s.

• quotient : α

  The quotient q.

• remainder : α

  The remainder r.

structure MvPolynomial.SetPseudoResult (α : Type u_1) : Type u_1

The result of pseudo-dividing g by a sequence of polynomials (a triangular set) satisfying the equation (∏ i, (S i).initial ^ es[i]) * g = (∑ i, qs[i] * S i) + r.

• exponents : List ℕ

  The powers of the initials es.

• quotients : List α

  The quotients qs.

• remainder : α

  The remainder r.

@[irreducible]

noncomputable def MvPolynomial.pseudoOf.go {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) (f : MvPolynomial σ R) (s : ℕ) (q r : MvPolynomial σ R) (h : degreeOf i f ≠ 0) : PseudoResult (MvPolynomial σ R)

The recursive algorithm of pseudo-division

Equations

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

noncomputable def MvPolynomial.pseudoOf {R : Type u_1} {σ : Type u_2} [CommRing R] (g : MvPolynomial σ R) [NoZeroDivisors R] (i : σ) (f : MvPolynomial σ R) : PseudoResult (MvPolynomial σ R)

Pseudo-division of g by f regarding the variable i. This algorithm computes q and r such that initᵢ(f) ^ s * g = q * f + r, where degᵢ(r) < degᵢ(f). It uses a fuel parameter to guarantee termination.

Equations

• g.pseudoOf i f = if h : MvPolynomial.degreeOf i f = 0 then { exponent := 1, quotient := g, remainder := 0 } else MvPolynomial.pseudoOf.go i f 0 0 g h

theorem MvPolynomial.zero_pseudoOf {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) (f : MvPolynomial σ R) : pseudoOf 0 i f = { exponent := 1 - degreeOf i f, quotient := 0, remainder := 0 }

theorem MvPolynomial.pseudoOf_self {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) (f : MvPolynomial σ R) : f.pseudoOf i f = { exponent := 1, quotient := initialOf i f, remainder := 0 }

theorem MvPolynomial.pseudoOfGo_next {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) (f : MvPolynomial σ R) (h : degreeOf i f ≠ 0) (s : ℕ) (q : MvPolynomial σ R) {r : MvPolynomial σ R} (hn : degreeOf i f ≤ degreeOf i r) : have term := initialOf i r * X i ^ (degreeOf i r - degreeOf i f); pseudoOf.go i f s q r h = pseudoOf.go i f (s + 1) (initialOf i f * q + term) (initialOf i f * r - term * f) h

theorem MvPolynomial.pseudoOfGo_equation {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) (g f : MvPolynomial σ R) (h : degreeOf i f ≠ 0) (s : ℕ) (q r : MvPolynomial σ R) : initialOf i f ^ s * g = q * f + r → initialOf i f ^ (pseudoOf.go i f s q r h).exponent * g = (pseudoOf.go i f s q r h).quotient * f + (pseudoOf.go i f s q r h).remainder

theorem MvPolynomial.pseudoOf_equation {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) (g f : MvPolynomial σ R) : initialOf i f ^ (g.pseudoOf i f).exponent * g = (g.pseudoOf i f).quotient * f + (g.pseudoOf i f).remainder

The fundamental equation of pseudo-division: initᵢ(f) ^ s * g = q * f + r

theorem MvPolynomial.degreeOf_pseudoOfGo_remainder_le_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i j : σ} {f : MvPolynomial σ R} (h : degreeOf i f ≠ 0) (hi : i ≠ j) (hj : degreeOf j f = 0) (s : ℕ) (q r : MvPolynomial σ R) : degreeOf j (pseudoOf.go i f s q r h).remainder ≤ degreeOf j r

theorem MvPolynomial.degreeOf_pseudoOf_remainder_le_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i j : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (hi : i ≠ j) (hj : degreeOf j f = 0) : degreeOf j (g.pseudoOf i f).remainder ≤ degreeOf j g

theorem MvPolynomial.dvd_pseudoOf_remainder_of_dvd {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] (i : σ) {g f : MvPolynomial σ R} (h : f ∣ g) : f ∣ (g.pseudoOf i f).remainder

theorem MvPolynomial.pseudoOf_remainder_eq_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} {g f : MvPolynomial σ R} (h1 : degreeOf i g = 0) (h2 : degreeOf i f ≠ 0) : (g.pseudoOf i f).remainder = g

theorem MvPolynomial.degreeOf_pseudoOfGo_remainder_lt_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} {f : MvPolynomial σ R} (h : degreeOf i f ≠ 0) (s : ℕ) (q r : MvPolynomial σ R) : degreeOf i (pseudoOf.go i f s q r h).remainder < degreeOf i f

theorem MvPolynomial.degreeOf_pseudoOf_remainder_lt_of_degreeOf_ne_zero {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (h : degreeOf i f ≠ 0) : degreeOf i (g.pseudoOf i f).remainder < degreeOf i f

theorem MvPolynomial.pseudoOf_remainder_eq_zero_of_dvd {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] {i : σ} {g f : MvPolynomial σ R} (h1 : f ∣ g) (h2 : degreeOf i f ≠ 0) : (g.pseudoOf i f).remainder = 0

theorem MvPolynomial.pseudoOf_remainder_reducedTo {R : Type u_1} {σ : Type u_2} [CommRing R] [NoZeroDivisors R] [DecidableEq R] [LinearOrder σ] {c : σ} (g : MvPolynomial σ R) {f : MvPolynomial σ R} (hc : f.vars.max = ↑c) : (g.pseudoOf c f).remainder.reducedTo f

def MvPolynomial.IsRemainder {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g f : MvPolynomial σ R) : Prop

A remainder r of g by f is a polynomial which is reduced with respect to f and suffices f.initial ^ s * g = q * f + r for some s : ℕ and q : MvPolynomial σ R.

Equations

• r.IsRemainder g f = (r.reducedTo f ∧ ∃ (s : ℕ) (q : MvPolynomial σ R), f.initial ^ s * g = q * f + r)

theorem MvPolynomial.isRemainder_def {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g f : MvPolynomial σ R) : r.IsRemainder g f ↔ r.reducedTo f ∧ ∃ (s : ℕ) (q : MvPolynomial σ R), f.initial ^ s * g = q * f + r

def MvPolynomial.IsSetRemainder {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g : MvPolynomial σ R) (S : TriangularSet σ R) : Prop

A remainder r of g by S is a polynomial which is reduced with respect to S and suffices (∏ i, (S i).initial ^ es[i]) * g = (∑ i, qs[i] * S i) + r for some es : List ℕ and qs : List (MvPolynomial σ R).

Equations

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

theorem MvPolynomial.isSetRemainder_def {R : Type u_1} {σ : Type u_2} [CommRing R] [DecidableEq R] [LinearOrder σ] (r g : MvPolynomial σ R) (S : TriangularSet σ R) : r.IsSetRemainder g S ↔ r.reducedToSet S ∧ ∃ (es : List ℕ) (qs : List (MvPolynomial σ R)), (es.length = S.length ∧ qs.length = S.length) ∧ (∏ i : Fin es.length, (S ↑i).initial ^ es[i]) * g = ∑ i : Fin qs.length, qs[i] * S ↑i + r

noncomputable def MvPolynomial.pseudo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) : PseudoResult (MvPolynomial σ R)

General pseudo-division of g by f. If f is constant, it performs standard division. If f is non-constant, it performs pseudo-division with respect to max_vars(f).

Equations

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

@[simp]

theorem MvPolynomial.pseudo_zero {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g : MvPolynomial σ R} : g.pseudo 0 = { exponent := 0, quotient := 0, remainder := g }

@[simp]

theorem MvPolynomial.pseudo_C {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g : MvPolynomial σ R} {r : R} (hr : r ≠ 0) : g.pseudo (C r) = { exponent := 0, quotient := r⁻¹ • g, remainder := 0 }

@[simp]

theorem MvPolynomial.zero_pseudo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : MvPolynomial σ R) : pseudo 0 f = { exponent := 0, quotient := 0, remainder := 0 }

@[simp]

theorem MvPolynomial.pseudo_remainder_self {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : MvPolynomial σ R) : (f.pseudo f).remainder = 0

theorem MvPolynomial.pseudo_of_max_vars_isSome {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) {c : σ} {f : MvPolynomial σ R} : f.vars.max = ↑c → g.pseudo f = g.pseudoOf c f

theorem MvPolynomial.pseudo_equation {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) : f.initial ^ (g.pseudo f).exponent * g = (g.pseudo f).quotient * f + (g.pseudo f).remainder

theorem MvPolynomial.degreeOf_pseudo_remainder_le_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) {i : σ} {f : MvPolynomial σ R} (h : degreeOf i f = 0) : degreeOf i (g.pseudo f).remainder ≤ degreeOf i g

theorem MvPolynomial.pseudo_remainder_reducedTo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) (h : f ≠ 0) : (g.pseudo f).remainder.reducedTo f

theorem MvPolynomial.pseudo_remainder_isRemainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g f : MvPolynomial σ R) (h : f ≠ 0) : (g.pseudo f).remainder.IsRemainder g f

theorem MvPolynomial.isRemainder_of_eq_pseudo_remainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {r g f : MvPolynomial σ R} (h : f ≠ 0) : (g.pseudo f).remainder = r → r.IsRemainder g f

theorem MvPolynomial.pseudo_remainder_eq_zero_of_dvd {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g f : MvPolynomial σ R} (h : f ∣ g) : (g.pseudo f).remainder = 0

theorem MvPolynomial.pseudo_remainder_eq_of_degreeOf_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {g f : MvPolynomial σ R} {c : σ} (h1 : f.vars.max = some c) (h2 : degreeOf c g = 0) : (g.pseudo f).remainder = g

@[irreducible]

noncomputable def MvPolynomial.setPseudo.go {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : ℕ → MvPolynomial σ R) (fuel : ℕ) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : SetPseudoResult (MvPolynomial σ R)

The recursive algorithm of successive pseudo-division by a triangular set

Equations

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

noncomputable def MvPolynomial.setPseudo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : SetPseudoResult (MvPolynomial σ R)

Pseudo-divides g successively by elements of S. Typically, this involves dividing by Sₗ₋₁, then Sₗ₋₂, ..., down to S₀.

Equations

• g.setPseudo S = MvPolynomial.setPseudo.go (⇑S) S.length [] [] g

theorem MvPolynomial.length_setPseudoGo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (f : ℕ → MvPolynomial σ R) (fuel : ℕ) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : (setPseudo.go f fuel es qs r).exponents.length = es.length + fuel ∧ (setPseudo.go f fuel es qs r).quotients.length = qs.length + fuel

theorem MvPolynomial.length_setPseudo_exponents {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : (g.setPseudo S).exponents.length = S.length

theorem MvPolynomial.length_setPseudo_quotients {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : (g.setPseudo S).quotients.length = S.length

theorem MvPolynomial.setPseudoGo_equation {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (f : ℕ → MvPolynomial σ R) (fuel : ℕ) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : List.foldrIdx (fun (i e : ℕ) (I : MvPolynomial σ R) => (f i).initial ^ e * I) 1 es fuel * g = List.foldrIdx (fun (i : ℕ) (q Q : MvPolynomial σ R) => q * f i + Q) 0 qs fuel + r → List.foldrIdx (fun (i e : ℕ) (I : MvPolynomial σ R) => (f i).initial ^ e * I) 1 (setPseudo.go f fuel es qs r).exponents * g = List.foldrIdx (fun (i : ℕ) (q Q : MvPolynomial σ R) => q * f i + Q) 0 (setPseudo.go f fuel es qs r).quotients + (setPseudo.go f fuel es qs r).remainder

theorem MvPolynomial.setPseudo_equation' {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : List.foldrIdx (fun (i e : ℕ) (I : MvPolynomial σ R) => (S i).initial ^ e * I) 1 (g.setPseudo S).exponents * g = List.foldrIdx (fun (i : ℕ) (q Q : MvPolynomial σ R) => q * S i + Q) 0 (g.setPseudo S).quotients + (g.setPseudo S).remainder

theorem MvPolynomial.setPseudo_equation {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : (∏ i : Fin (g.setPseudo S).exponents.length, (S ↑i).initial ^ (g.setPseudo S).exponents[i]) * g = ∑ i : Fin (g.setPseudo S).quotients.length, (g.setPseudo S).quotients[i] * S ↑i + (g.setPseudo S).remainder

noncomputable def MvPolynomial.setPseudoRem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : MvPolynomial σ R

The remainder of pseudo-dividing g by the set S. This is computationally simpler than setPseudo if only the remainder is needed.

Equations

• g.setPseudoRem S = List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) g S.toList

theorem MvPolynomial.zero_setPseudoRem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) : List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) 0 l = 0

theorem MvPolynomial.setPseudoGo_drop_succ_remainder_eq {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (S : TriangularSet σ R) {k n : ℕ} (hn : n < k) (hk : k ≤ S.length) (es : List ℕ) (qs : List (MvPolynomial σ R)) (r : MvPolynomial σ R) : (setPseudo.go (⇑(S.drop (k - (n + 1)))) (n + 1) es qs r).remainder = ((setPseudo.go (⇑(S.drop (k - n))) n es qs r).remainder.pseudo (S (k - (n + 1)))).remainder

theorem MvPolynomial.setPseudo_remainder_eq_setPseudoRem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : (g.setPseudo S).remainder = g.setPseudoRem S

theorem MvPolynomial.setPseudoRem_reducedTo {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (hl1 : ∀ ⦃p : MvPolynomial σ R⦄, p ∈ l → p ≠ 0) (hl2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.vars.max < q.vars.max) l) (g p : MvPolynomial σ R) : p ∈ l → (List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) g l).reducedTo p

theorem MvPolynomial.setPseudo_remainder_reducedToSet {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : (g.setPseudo S).remainder.reducedToSet S

theorem MvPolynomial.setPseudo_remainder_isSetRemainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (g : MvPolynomial σ R) (S : TriangularSet σ R) : (g.setPseudo S).remainder.IsSetRemainder g S

theorem MvPolynomial.isSetRemainder_of_eq_setPseudo_remainder {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] {r g : MvPolynomial σ R} {S : TriangularSet σ R} : (g.setPseudo S).remainder = r → r.IsSetRemainder g S

theorem MvPolynomial.setPseudoRem_eq_self_of_max_vars_lt {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (hl1 : ∀ ⦃p : MvPolynomial σ R⦄, p ∈ l → p ≠ 0) (hl2 : List.Pairwise (fun (p q : MvPolynomial σ R) => p.vars.max < q.vars.max) l) ⦃g : MvPolynomial σ R⦄ : (∀ p ∈ l, g.vars.max < p.vars.max) → List.foldr (fun (p r : MvPolynomial σ R) => (r.pseudo p).remainder) g l = g

theorem MvPolynomial.setPseudo_remainder_eq_zero_of_mem {R : Type u_1} {σ : Type u_2} [Field R] [DecidableEq R] [LinearOrder σ] (S : TriangularSet σ R) {p : MvPolynomial σ R} (hp : p ∈ S) : (p.setPseudo S).remainder = 0