Reduction relation

This file defines the reduction relation between multivariate polynomials, a fundamental concept in the Characteristic Set Method.

Main definitions

• MvPolynomial.reducedTo q p: A polynomial q is reduced with respect to p if either q = 0 or the degree of q in p's main variable is strictly less than the degree of p. If p is a constant (i.e., max_vars p = ⊥), then no non-zero q is reduced w.r.t. p.

• MvPolynomial.reducedToSet q a: A polynomial q is reduced with respect to a set a if it is reduced with respect to every element of a.

def MvPolynomial.reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (q p : MvPolynomial σ R) : Prop

q is reduced with respect to pif q = 0 or if the degree of q in the main variable of p is strictly less than the degree of p.

Note: if p is a constant, then no non-zero q is reduced with respect to p.

Equations

• q.reducedTo p = if q = 0 then True else match p.vars.max with | none => False | some c => MvPolynomial.degreeOf c q < MvPolynomial.degreeOf c p

theorem MvPolynomial.zero_reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (p : MvPolynomial σ R) : reducedTo 0 p

theorem MvPolynomial.not_reducedTo_of_bot_max_vars {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (hq : q ≠ 0) : p.vars.max = ⊥ → ¬q.reducedTo p

theorem MvPolynomial.max_vars_ne_bot_of_reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (hq : q ≠ 0) : q.reducedTo p → p.vars.max ≠ ⊥

theorem MvPolynomial.reducedTo_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} {c : σ} (hp : p.vars.max = ↑c) (hq : q ≠ 0) : q.reducedTo p ↔ degreeOf c q < degreeOf c p

@[implicit_reducible]

noncomputable instance MvPolynomial.instDecidableRelReducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : DecidableRel reducedTo

Equations

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

theorem MvPolynomial.reducedTo_of_max_vars_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (h : q.vars.max < p.vars.max) : q.reducedTo p

theorem MvPolynomial.reducedTo_congr_right {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q r : MvPolynomial σ R} (h : p ≈ q) : r.reducedTo p ↔ r.reducedTo q

theorem MvPolynomial.reducedTo_iff_gt_of_max_vars_eq {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (hq : q ≠ 0) (h : q.vars.max = p.vars.max) : q.reducedTo p ↔ q < p

theorem MvPolynomial.not_reduceTo_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (h : p ≠ 0) : ¬p.reducedTo p

theorem MvPolynomial.max_vars_lt_of_reducedTo_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (h1 : q ≠ 0) (h2 : p ≤ q) (h3 : q.reducedTo p) : p.vars.max < q.vars.max

theorem MvPolynomial.lt_of_reducedTo_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} (h1 : q ≠ 0) (h2 : p ≤ q) (h3 : q.reducedTo p) : p < q

def MvPolynomial.reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] (q : MvPolynomial σ R) (a : α) : Prop

q is reduced with respect to a set a if it is reduced with respect to all elements of a.

Equations

• q.reducedToSet a = ∀ p ∈ a, q.reducedTo p

@[implicit_reducible]

noncomputable instance MvPolynomial.instDecidableRelListReducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : DecidableRel reducedToSet

Equations

• x✝.instDecidableRelListReducedToSet = List.decidableBAll x✝.reducedTo

theorem MvPolynomial.reducedToSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] {q : MvPolynomial σ R} {a : α} : q.reducedToSet a ↔ ∀ p ∈ a, q.reducedTo p

theorem MvPolynomial.zero_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_3} [Membership (MvPolynomial σ R) α] {a : α} : reducedToSet 0 a

theorem MvPolynomial.initial_reducedTo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p q : MvPolynomial σ R} : q.reducedTo p → q.initial.reducedTo p

theorem MvPolynomial.initial_reducedTo_self {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {p : MvPolynomial σ R} (hp : p.vars.max ≠ ⊥) : p.initial.reducedTo p

theorem MvPolynomial.initial_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {α : Type u_4} [Membership (MvPolynomial σ R) α] {p : MvPolynomial σ R} {a : α} : p.reducedToSet a → p.initial.reducedToSet a

theorem MvPolynomial.reducedToSet_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (q : MvPolynomial σ R) : q.reducedToSet ∅

theorem MvPolynomial.reducedToSet_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {q : MvPolynomial σ R} : q.reducedToSet S ↔ ∀ i < S.length, q.reducedTo (S i)

@[implicit_reducible]

noncomputable instance MvPolynomial.instDecidableRelReducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : DecidableRel reducedToSet

Equations

• x✝.instDecidableRelReducedToSet S = decidable_of_iff (∀ i < S.length, x✝.reducedTo (S i)) ⋯

theorem MvPolynomial.reducedToSet_congr_right {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S T : TriangularSet σ R} {q : MvPolynomial σ R} : S ≈ T → (q.reducedToSet S ↔ q.reducedToSet T)

theorem TriangularSet.takeConcat_lt_of_reducedToSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (p_ne_zero : p ≠ 0) (hp : p.reducedToSet S) : S.takeConcat p < S

Key Lemma for the Basic Set Algorithm: If p is non-zero and reduced with respect to S, then modifying S by appending p (using takeConcat) strictly decreases the order of the triangular set. This order decrease is what guarantees the termination of the characteristic set computation.