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.mainVariable < p.mainVariable.

Main Instances

• 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 : TriangulatedSet σ 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 : TriangulatedSet σ 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 : TriangulatedSet σ R} {i j : ℕ} (h : isAscendingSet S) : i ≠ j → j < S.length → (S i).initial.reducedTo (S j)

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

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

theorem WeakAscendingSet.isAscendingSet_concat {R : Type u_1} {σ : Type u_2} [CommSemiring R] [DecidableEq R] [LinearOrder σ] {S : TriangulatedSet σ 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 : TriangulatedSet σ R} {p : MvPolynomial σ R} (hp : p.initial.reducedToSet S) : S.isAscendingSet → (S.takeConcat p).isAscendingSet

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

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

Equations

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

@[irreducible]

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

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 : TriangulatedSet σ 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 : TriangulatedSet σ 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 : TriangulatedSet σ 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 : TriangulatedSet σ 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 : TriangulatedSet σ 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 : TriangulatedSet σ 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

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.