Rank and Orderings on polynomials and triangular sets

This file defines rank structures on multivariate polynomials and triangular sets, which are essential for the Characteristic Set Method (Wu's Method).

Main definitions

• MvPolynomial.rank: The rank of a polynomial p is the pair (max_vars p, mainDegree.card p), ordered lexicographically. This defines a well-ordering on polynomials when the variable type is well-founded.

• TriangularSet.rank: The rank of a triangular set is a lexicographic sequence of ranks of its polynomials. For two triangular sets S and T, S < T if either:

  1. There exists k < S.length such that S₀ ≈ T₀, S₁ ≈ T₁, ..., Sₖ₋₁ ≈ Tₖ₋₁ and Sₖ < Tₖ;
  2. S.length > T.length and ∀ i < T.length, Sᵢ ≈ Tᵢ.

Main results

• MvPolynomial.instWellFoundedLT: When σ is well-founded, polynomials are well-founded under the rank ordering.

• TriangularSet.instWellFoundedLT: When σ is finite, triangular sets are well-founded under the rank ordering. This guarantees termination of characteristic set algorithms.

References

• [Wen-Tsun Wu, Basic principles of mechanical theorem proving in elementary geometries] [WT86]

noncomputable def MvPolynomial.rank {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (p : MvPolynomial σ R) : Lex (WithBot σ × ℕ)

The rank of a polynomial p is the pair (max_vars p, degree p), which is ordered lexicographically.

Equations

• p.rank = (p.vars.max, p.mainDegree.card)

theorem MvPolynomial.rank_eq_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p.rank = q.rank ↔ p.vars.max = q.vars.max ∧ p.mainDegree.card = q.mainDegree.card

@[instance_reducible]

instance MvPolynomial.instPreorder {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Preorder (MvPolynomial σ R)

Equations

• MvPolynomial.instPreorder = { le := InvImage (fun (x1 x2 : Lex (WithBot σ × ℕ)) => x1 ≤ x2) MvPolynomial.rank, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem MvPolynomial.le_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ p.rank ≤ q.rank

@[instance_reducible]

noncomputable instance MvPolynomial.instDecidableLE {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLE (MvPolynomial σ R)

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.rank ≤ x✝.rank) ⋯

@[instance_reducible]

noncomputable instance MvPolynomial.instDecidableLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLT (MvPolynomial σ R)

Equations

• MvPolynomial.instDecidableLT = decidableLTOfDecidableLE

instance MvPolynomial.instIsTotalLe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Std.Total LE.le

theorem MvPolynomial.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ p.vars.max < q.vars.max ∨ p.vars.max = q.vars.max ∧ p.mainDegree.card ≤ q.mainDegree.card

theorem MvPolynomial.le_iff_not_imp {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ ¬p.vars.max < q.vars.max → p.vars.max = q.vars.max ∧ p.mainDegree.card ≤ q.mainDegree.card

theorem MvPolynomial.max_vars_le_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q → p.vars.max ≤ q.vars.max

theorem MvPolynomial.lt_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p < q ↔ p.rank < q.rank

theorem MvPolynomial.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p < q ↔ p.vars.max < q.vars.max ∨ p.vars.max = q.vars.max ∧ p.mainDegree.card < q.mainDegree.card

theorem MvPolynomial.lt_iff_not_imp {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p < q ↔ ¬p.vars.max < q.vars.max → p.vars.max = q.vars.max ∧ p.mainDegree.card < q.mainDegree.card

theorem MvPolynomial.lt_of_max_vars_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p.vars.max < q.vars.max → p < q

@[simp]

theorem MvPolynomial.not_lt_iff_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : ¬p < q ↔ q ≤ p

@[simp]

theorem MvPolynomial.not_le_iff_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : ¬p ≤ q ↔ q < p

theorem MvPolynomial.X_lt_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] {i j : σ} : i < j → X i < X j

@[instance_reducible]

instance MvPolynomial.instSetoid {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Setoid (MvPolynomial σ R)

Equations

• MvPolynomial.instSetoid = AntisymmRel.setoid (MvPolynomial σ R) fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2

@[instance_reducible]

noncomputable instance MvPolynomial.instDecidableRelEquiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableRel fun (x1 x2 : MvPolynomial σ R) => x1 ≈ x2

Equations

• x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

theorem MvPolynomial.equiv_def'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ p ≤ q ∧ q ≤ p

theorem MvPolynomial.equiv_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ p.rank = q.rank

theorem MvPolynomial.equiv_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ ¬p < q ∧ ¬q < p

theorem MvPolynomial.equiv_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≈ q ↔ p.vars.max = q.vars.max ∧ p.mainDegree.card = q.mainDegree.card

theorem MvPolynomial.le_iff_lt_or_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q ↔ p < q ∨ p ≈ q

theorem MvPolynomial.lt_of_equiv_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q r : MvPolynomial σ R} : p ≈ q → q < r → p < r

theorem MvPolynomial.lt_of_lt_of_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q r : MvPolynomial σ R} : p < q → q ≈ r → p < r

theorem MvPolynomial.equiv_of_le_of_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p q : MvPolynomial σ R} : p ≤ q → q ≤ p → p ≈ q

theorem MvPolynomial.zero_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} : 0 ≤ p

theorem MvPolynomial.wellFoundedLT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (MvPolynomial σ R) → WellFoundedLT σ

instance MvPolynomial.instWellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT σ] : WellFoundedLT (MvPolynomial σ R)

theorem MvPolynomial.wellFoundedLT_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (MvPolynomial σ R) ↔ WellFoundedLT σ

theorem MvPolynomial.Set.has_min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) : ∃ p ∈ PS, ∀ q ∈ PS, ¬q < p

noncomputable def MvPolynomial.Set.min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) : MvPolynomial σ R

The minimal element of a nonempty set of multivariate polynomials.

Equations

• MvPolynomial.Set.min PS h = ⋯.choose

theorem MvPolynomial.Set.min_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [WellFoundedLT (MvPolynomial σ R)] (PS : Set (MvPolynomial σ R)) (h : PS.Nonempty) : min PS h ∈ PS

theorem MvPolynomial.reducedTo_congr_right {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {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] [LinearOrder σ] [DecidableEq R] {p q : MvPolynomial σ R} (hq : q ≠ 0) (h : q.vars.max = p.vars.max) : q.reducedTo p ↔ q < p

theorem MvPolynomial.max_vars_lt_of_reducedTo_of_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [DecidableEq R] {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] [LinearOrder σ] [DecidableEq R] {p q : MvPolynomial σ R} (h1 : q ≠ 0) (h2 : p ≤ q) (h3 : q.reducedTo p) : p < q

theorem TriangularSet.apply_lt_of_index_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} (h : n < S.length) : m < n → S m < S n

theorem TriangularSet.index_lt_of_apply_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} (h : m < S.length) : S m < S n → m < n

theorem TriangularSet.le_of_index_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {m n : ℕ} : m ≤ n → n < S.length → S m ≤ S n

noncomputable def TriangularSet.rank {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) : Lex (ℕ → WithTop (Lex (WithBot σ × ℕ)))

The rank of a Triangular Set is a lexicographic sequence of ranks of its polynomials. A more intuitive definition is rank_lt_iff, S < T if one of the following two occurs:

1. There exists some k < S.length such that S₀ ≈ T₀, S₁ ≈ T₁, ..., Sₖ₋₁ ≈ Tₖ₋₁ and Sₖ < Tₖ.
2. S.length > T.length and ∀ i < T.length, Sᵢ ≈ Tᵢ

Equations

• S.rank = toLex fun (i : ℕ) => if i < S.length then ↑(S i).rank else ⊤

theorem TriangularSet.rank_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} : S.rank = fun (i : ℕ) => if i < S.length then ↑(S i).rank else ⊤

theorem TriangularSet.rank_apply {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {i : ℕ} (h : i < S.length) : S.rank i = ↑(S i).rank

theorem TriangularSet.rank_apply' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {i : ℕ} (h : S.length ≤ i) : S.rank i = ⊤

theorem TriangularSet.rank_lt_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S.rank < T.rank ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length < S.length ∧ ∀ i < T.length, S i ≈ T i

theorem TriangularSet.rank_eq_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S.rank = T.rank ↔ S.length = T.length ∧ ∀ (k : ℕ), S k ≈ T k

theorem TriangularSet.rank_le_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S.rank ≤ T.rank ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length ≤ S.length ∧ ∀ k < T.length, S k ≤ T k

@[instance_reducible]

instance TriangularSet.instPreorder {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Preorder (TriangularSet σ R)

Equations

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

theorem TriangularSet.le_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T ↔ S.rank ≤ T.rank

@[instance_reducible]

noncomputable instance TriangularSet.instDecidableLE {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLE (TriangularSet σ R)

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.rank ≤ x✝.rank) ⋯

@[instance_reducible]

noncomputable instance TriangularSet.instDecidableLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableLT (TriangularSet σ R)

Equations

• TriangularSet.instDecidableLT = decidableLTOfDecidableLE

instance TriangularSet.instTotalLe {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Std.Total LE.le

theorem TriangularSet.le_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length ≤ S.length ∧ ∀ k < T.length, S k ≤ T k

theorem TriangularSet.lt_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S < T ↔ S.rank < T.rank

theorem TriangularSet.lt_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S < T ↔ (∃ k < S.length, S k < T k ∧ ∀ i < k, S i ≈ T i) ∨ T.length < S.length ∧ ∀ i < T.length, S i ≈ T i

theorem TriangularSet.lt_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} : S ≠ ∅ → S < ∅

theorem TriangularSet.le_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] (S : TriangularSet σ R) : S ≤ ∅

@[simp]

theorem TriangularSet.not_lt_iff_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : ¬S < T ↔ T ≤ S

@[simp]

theorem TriangularSet.not_le_iff_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : ¬S ≤ T ↔ T < S

theorem TriangularSet.ge_of_forall_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : (∀ n < S.length, ∃ i < T.length, T i ≈ S n) → T ≤ S

theorem TriangularSet.ge_of_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ⊆ T → T ≤ S

@[instance_reducible]

instance TriangularSet.instSetoid {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : Setoid (TriangularSet σ R)

Equations

• TriangularSet.instSetoid = AntisymmRel.setoid (TriangularSet σ R) fun (x1 x2 : TriangularSet σ R) => x1 ≤ x2

@[instance_reducible]

noncomputable instance TriangularSet.instDecidableRelEquiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : DecidableRel fun (x1 x2 : TriangularSet σ R) => x1 ≈ x2

Equations

• x✝¹.instDecidableRelEquiv x✝ = instDecidableAnd

theorem TriangularSet.equiv_def'' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S ≤ T ∧ T ≤ S

theorem TriangularSet.equiv_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S.rank = T.rank

theorem TriangularSet.equiv_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ ¬S < T ∧ ¬T < S

theorem TriangularSet.equiv_iff {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S.length = T.length ∧ ∀ (k : ℕ), S k ≈ T k

theorem TriangularSet.equiv_iff' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≈ T ↔ S.length = T.length ∧ ∀ k < S.length, S k ≈ T k

theorem TriangularSet.le_iff_lt_or_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T ↔ S < T ∨ S ≈ T

theorem TriangularSet.lt_of_equiv_of_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T U : TriangularSet σ R} : S ≈ T → T < U → S < U

theorem TriangularSet.lt_of_lt_of_equiv {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T U : TriangularSet σ R} : S < T → T ≈ U → S < U

theorem TriangularSet.equiv_of_le_of_ge {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ≤ T → T ≤ S → S ≈ T

theorem TriangularSet.gt_of_ssubset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} : S ⊂ T → T < S

theorem TriangularSet.lt_take {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} : n < S.length → S < S.take n

theorem TriangularSet.lt_drop {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {n : ℕ} : S ≠ ∅ → 0 < n → S < S.drop n

theorem TriangularSet.concat_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) : S.concat p h < S

theorem TriangularSet.single_lt_empty {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} [DecidableEq R] : p ≠ 0 → single p < ∅

theorem TriangularSet.gt_single_of_first_gt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {p : MvPolynomial σ R} {S : TriangularSet σ R} [DecidableEq R] : p ≠ 0 → p < S 0 → single p < S

Well-Foundedness

theorem TriangularSet.wellFoundedLT_mvPolynomial_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] : WellFoundedLT (TriangularSet σ R) → WellFoundedLT (MvPolynomial σ R)

theorem TriangularSet.wellFoundedLT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (TriangularSet σ R) → WellFoundedLT σ

theorem TriangularSet.wellFoundedGT_variables_of_wellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Nontrivial R] : WellFoundedLT (TriangularSet σ R) → WellFoundedGT σ

theorem TriangularSet.length_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S : TriangularSet σ R} [Fintype σ] : S.length ≤ Fintype.card σ + 1

instance TriangularSet.instIsWellFoundedOrderLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] : WellFounded (InvImage (fun (x1 x2 : Lex (ℕ → WithTop (Lex (WithBot σ × ℕ)))) => x1 < x2) rank)

The set of Triangular Sets is well-founded under the lexicographic rank ordering. This is a crucial result that guarantees the termination of the Characteristic Set Algorithm.

instance TriangularSet.instWellFoundedLT {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] : WellFoundedLT (TriangularSet σ R)

@[instance_reducible]

instance TriangularSet.instWellFoundedRelation {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] : WellFoundedRelation (TriangularSet σ R)

Equations

• TriangularSet.instWellFoundedRelation = { rel := fun (x1 x2 : TriangularSet σ R) => x1 < x2, wf := ⋯ }

theorem TriangularSet.Set.has_min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) : ∃ S ∈ S', ∀ T ∈ S', S ≤ T

noncomputable def TriangularSet.Set.min {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) : TriangularSet σ R

The minimal element of a nonempty set of triangular sets.

Equations

• TriangularSet.Set.min S' h = ⋯.choose

theorem TriangularSet.Set.min_mem {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) : min S' h ∈ S'

theorem TriangularSet.Set.min_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] [Finite σ] (S' : Set (TriangularSet σ R)) (h : S'.Nonempty) (T : TriangularSet σ R) : T ∈ S' → min S' h ≤ T

theorem TriangularSet.reducedToSet_congr_right {R : Type u_1} {σ : Type u_2} [CommSemiring R] [LinearOrder σ] {S T : TriangularSet σ R} [DecidableEq 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] [LinearOrder σ] {S : TriangularSet σ R} [DecidableEq 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.