Weak Ascending Set (Wu's Definition)

This file implements the theory and algorithm for Weak Ascending Set, which are central to Wu's Method. In this context, a "Weak Ascending Set" requires that the initial of every element is reduced with respect to preceding elements. This is a weaker condition than the standard reduction.

Consequently, the algorithm for computing a Weak Basic Set must ensure the triangular structure (strict ascending main variables) explicitly, by filtering candidates with B.max_vars < p.max_vars.

Main declarations

• AscendingSetTheory: Implements the theory using initial.reducedTo (weak reduction).
• HasBasicSet: Provides the basicSet algorithm that computes a minimal weak ascending set.

theorem WeakAscendingSet.isAscendingSet_def {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} : IsAscendingSet S ↔ ∀ ⦃i j : ℕ⦄, i < j → j < S.length → (S j).initial.reducedTo (S i)

theorem WeakAscendingSet.isAscendingSet_def' {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} : IsAscendingSet S ↔ ∀ ⦃i j : ℕ⦄, i < j → i < S.length → (S j).initial.reducedTo (S i)

theorem WeakAscendingSet.initial_reducedTo_of_ne {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {i j : ℕ} (h : IsAscendingSet S) : i ≠ j → j < S.length → (S i).initial.reducedTo (S j)

@[implicit_reducible]

noncomputable def WeakAscendingSet.instAscendingSetTheory {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : AscendingSetTheory σ R

The weak ascending set theory uses weak reduction p.initial.reducedTo.

Equations

• WeakAscendingSet.instAscendingSetTheory = { reducedTo' := fun (p : MvPolynomial σ R) => p.initial.reducedTo, decidableReducedTo := inferInstance, initial_reducedToSet_of_max_vars_ne_bot := ⋯ }

theorem WeakAscendingSet.isAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (h : S.CanConcat p) (hp : p.initial.reducedToSet S) : S.IsAscendingSet → (S.concat p h).IsAscendingSet

theorem WeakAscendingSet.isAscendingSet_takeConcat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangularSet σ R} {p : MvPolynomial σ R} (hp : p.initial.reducedToSet S) : S.IsAscendingSet → (S.takeConcat p).IsAscendingSet

@[irreducible]

noncomputable def WeakAscendingSet.basicSet.go {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : TriangularSet σ R

The recursive algorithm for computing the Weak Basic Set.

Equations

• One or more equations did not get rendered due to their size.
• WeakAscendingSet.basicSet.go [] BS hl1_2 hl2_2 = BS

noncomputable def WeakAscendingSet.basicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) : TriangularSet σ R

Computes the Weak Basic Set of a list of polynomials. Difference from Standard: The filter condition includes B.max_vars < p.max_vars. This is because p.initial.reducedTo B does NOT imply B.max_vars < p.max_vars (unlike strong reduction). We must enforce the triangular structure explicitly.

Equations

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

theorem WeakAscendingSet.basicSetGo_lt {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) (h : l ≠ []) : (l.head h).initial.reducedToSet BS → basicSet.go l BS hl1 hl2 < BS

theorem WeakAscendingSet.basicSetGo_le {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : Option.all (fun (p : MvPolynomial σ R) => decide (p.initial.reducedToSet BS)) l.head? = true → basicSet.go l BS hl1 hl2 ≤ BS

theorem WeakAscendingSet.mem_of_mem_basicSetGo {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) (p : MvPolynomial σ R) : p ∉ BS → p ∈ basicSet.go l BS hl1 hl2 → p ∈ l

theorem WeakAscendingSet.basicSetGo_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : Option.all (fun (p : MvPolynomial σ R) => decide (p.initial.reducedToSet BS)) l.head? = true → BS.IsAscendingSet → (basicSet.go l BS hl1 hl2).IsAscendingSet

theorem WeakAscendingSet.basicSetGo_le_ascendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) (BS : TriangularSet σ R) (hl1 : ∀ p ∈ l, p ≠ 0) (hl2 : ∀ p ∈ l, BS.CanConcat p) : List.Pairwise (fun (x1 x2 : MvPolynomial σ R) => x1 ≤ x2) l → Option.all (fun (p : MvPolynomial σ R) => decide (p.initial.reducedToSet BS)) l.head? = true → ∀ (T : TriangularSet σ R), T.IsAscendingSet → (BS.length ≤ T.length ∧ ∀ i < BS.length, BS i ≈ T i) → (∀ p ∈ T, (∀ i < BS.length, ¬BS i ≈ p) → p ∈ l) → basicSet.go l BS hl1 hl2 ≤ T

theorem WeakAscendingSet.basicSet_isAscendingSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) : (basicSet l).IsAscendingSet

theorem WeakAscendingSet.basicSet_subset {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) ⦃p : MvPolynomial σ R⦄ : p ∈ basicSet l → p ∈ l

theorem WeakAscendingSet.basicSet_minimal {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] (l : List (MvPolynomial σ R)) ⦃S : TriangularSet σ R⦄ : S.IsAscendingSet → (∀ ⦃p : MvPolynomial σ R⦄, p ∈ S → p ∈ l) → basicSet l ≤ S

@[implicit_reducible]

noncomputable def WeakAscendingSet.instHasBasicSet {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] : HasBasicSet σ R

The Weak Basic Set algorithm satisfies the abstract HasBasicSet interface.

Equations

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