The DGH stratification closes at ε₀

For any ring R and any M ⊆ R, the Dubrovin–Gräter–Hanke stratum D M ε₀ is closed under sums, products and inverses of its units of R (κ ≤ ε₀).

Proof sketch

Three monotone potentials, one per process, each written as the minimum of a failure set:

• iota x = min {c | invSet (D c) ⊄ D x}, capped at A + 1;
• piHat x = min {h(t.map iota) | t ∈ N(Q), prodSets t ⊄ D x}, capped at ω^(A+2);
• sigHat x = min {h(t.map mu) | t ∈ N(S), sumSets t ⊄ D x}, capped at ω^(B+1),

with mu = iota ♯ piHat, h the Hessenberg value, and Q / S the successors of inverse / (inverse or product) steps. Substitution lemmas put the chosen multisets in N(Q) / N(S); on Q / S the labels iota / mu are strictly increasing, so they preserve Jakobs' order. Then Phi = mu ♯ sigHat is strictly increasing on [1, ε₀) and bounded by some β < ε₀: impossible.

Main results

• kappa_le_epsilon0;
• sum_entry, prod_entry, D_stationary, main_contra, nadd_lt_epsilon_zero, jakobsLT_map.

1. Natural sum: monotonicity and closure below ε₀

theorem DGH.lt_opow_add_one (o : Ordinal.{0}) {Λ : Ordinal.{0}} (h : o ≤ Λ) : o < Ordinal.omega0 ^ (Λ + 1)

theorem DGH.exists_hval_eq (o : Ordinal.{0}) {Λ : Ordinal.{0}} (h : o ≤ Λ) : ∃ (s : Multiset Ordinal.{0}), (∀ x ∈ s, x ≤ Λ) ∧ hval s = o

theorem DGH.nadd_lt_nadd_right {a b : Ordinal.{0}} (h : a < b) (c : Ordinal.{0}) : nadd a c < nadd b c

theorem DGH.nadd_lt_nadd_left {a b : Ordinal.{0}} (h : a < b) (c : Ordinal.{0}) : nadd c a < nadd c b

theorem DGH.nadd_le_nadd {a b c d : Ordinal.{0}} (h1 : a ≤ b) (h2 : c ≤ d) : nadd a c ≤ nadd b d

theorem DGH.nadd_lt_of_lt_of_le {a b c d : Ordinal.{0}} (h1 : a < b) (h2 : c ≤ d) : nadd a c < nadd b d

theorem DGH.nadd_lt_of_le_of_lt {a b c d : Ordinal.{0}} (h1 : a ≤ b) (h2 : c < d) : nadd a c < nadd b d

theorem DGH.nadd_lt_epsilon_zero {a b : Ordinal.{0}} (ha : a < Ordinal.epsilon 0) (hb : b < Ordinal.epsilon 0) : nadd a b < Ordinal.epsilon 0

ε₀ is closed under the natural sum.

theorem DGH.succ_lt_epsilon_zero {x : Ordinal.{0}} (h : x < Ordinal.epsilon 0) : x + 1 < Ordinal.epsilon 0

2. Jakobs' order: relabeling and a bound

theorem DGH.jakobsLT_map {T : Set Ordinal.{0}} {f : Ordinal.{0} → Ordinal.{0}} (hf : ∀ x ∈ T, ∀ y ∈ T, x < y → f x < f y) {s t : Multiset Ordinal.{0}} (hs : ∀ x ∈ s, x ∈ T) (ht : ∀ x ∈ t, x ∈ T) (h : jakobsLT s t) : jakobsLT (Multiset.map f s) (Multiset.map f t)

Relabeling: a map strictly increasing on a set containing the supports preserves Jakobs' order.

theorem DGH.le_of_jakobsLT {s t : Multiset Ordinal.{0}} (h : jakobsLT t s) {a : Ordinal.{0}} (hs : ∀ x ∈ s, x ≤ a) (y : Ordinal.{0}) : y ∈ t → y ≤ a

If t <_J s, every entry of t is bounded by a bound of the entries of s.

3. Potentials: minimum of a failure set, capped

noncomputable def DGH.pot (V : Set Ordinal.{0}) (top : Ordinal.{0}) : Ordinal.{0}

pot V top = min (V ∪ {top}).

Equations

• DGH.pot V top = sInf (insert top V)

theorem DGH.pot_le_top (V : Set Ordinal.{0}) (top : Ordinal.{0}) : pot V top ≤ top

theorem DGH.pot_le_of_mem {V : Set Ordinal.{0}} {top v : Ordinal.{0}} (h : v ∈ V) : pot V top ≤ v

theorem DGH.pot_anti {V V' : Set Ordinal.{0}} {top : Ordinal.{0}} (h : V' ⊆ V) : pot V top ≤ pot V' top

theorem DGH.lt_pot {V : Set Ordinal.{0}} {top v : Ordinal.{0}} (htop : v < top) (h : ∀ w ∈ V, v < w) : v < pot V top

theorem DGH.no_bounded_strictMono (F : Ordinal.{0} → Ordinal.{0}) {β : Ordinal.{0}} (hβ : β < Ordinal.epsilon 0) (hF : ∀ (x y : Ordinal.{0}), 1 ≤ x → x < y → y < Ordinal.epsilon 0 → F x < F y) (hb : ∀ (x : Ordinal.{0}), F x ≤ β) : False

A map strictly increasing on [1, ε₀) cannot be bounded by some β < ε₀.

4. Ring-level helpers

theorem DGH.zero_mem_D {R : Type} [Ring R] (M : Set R) (x : Ordinal.{0}) : 0 ∈ D M x

theorem DGH.one_mem_D {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} (hx : x ≠ 0) : 1 ∈ D M x

theorem DGH.sumSets_cons {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) (s : Multiset Ordinal.{0}) : sumSets E (a ::ₘ s) = E a + sumSets E s

theorem DGH.sumSets_add' {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (s t : Multiset Ordinal.{0}) : sumSets E (s + t) = sumSets E s + sumSets E t

theorem DGH.sumSets_zero {R : Type} [Ring R] (E : Ordinal.{0} → Set R) : sumSets E 0 = 0

theorem DGH.sumSets_singleton {R : Type} [Ring R] (E : Ordinal.{0} → Set R) (a : Ordinal.{0}) : sumSets E {a} = E a

5. Primitivity (P2): substitution lemma for sums

theorem DGH.sum_subst {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : s ∈ sumCand (D M) x) (hmin : ∀ t ∈ sumCand (D M) x, ¬t.IsDershowitzMannaLT s) {d : Ordinal.{0}} (hd : d ∈ s) (hsub : ∀ u ∈ D M d, ∃ (r : Multiset Ordinal.{0}), (∀ y ∈ r, y < d) ∧ u ∈ sumSets (D M) r) : False

Substitution lemma (sum).

theorem DGH.sum_entry {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : s ∈ sumCand (D M) x) (hmin : ∀ t ∈ sumCand (D M) x, ¬t.IsDershowitzMannaLT s) {d : Ordinal.{0}} (hd : d ∈ s) : d = 1 ∨ ∃ (a : Ordinal.{0}), d = Order.succ a ∧ a ≠ 0 ∧ SumClosed (D M a) ∧ ¬(MulClosed (D M a) ∧ InvClosed (D M a))

(P2) The entries of the chosen multiset of a sum step are 1 or successors of product / inverse steps.

6. Primitivity (P1): substitution lemma for products

theorem DGH.prod_core {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} (hx : x ≠ 0) {s : Multiset Ordinal.{0}} (hs : s ∈ prodCand (D M) x) (hmin : ∀ t ∈ prodCand (D M) x, ¬t.IsDershowitzMannaLT s) {l1 l2 : List Ordinal.{0}} {d : Ordinal.{0}} (hl : ↑(l1 ++ d :: l2) = s) {m : List Ordinal.{0}} (hm : ∀ y ∈ m, y < d) {p u q : R} (hp : p ∈ (List.map (D M) l1).prod) (hu : u ∈ (List.map (D M) m).prod) (hq : q ∈ (List.map (D M) l2).prod) : p * (u * q) ∈ D M x

Core substitution (product): replacing the factor d by a word in strata < d.

theorem DGH.prod_core_single {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} (hx : x ≠ 0) {s : Multiset Ordinal.{0}} (hs : s ∈ prodCand (D M) x) (hmin : ∀ t ∈ prodCand (D M) x, ¬t.IsDershowitzMannaLT s) {l1 l2 : List Ordinal.{0}} {d : Ordinal.{0}} (hl : ↑(l1 ++ d :: l2) = s) {e : Ordinal.{0}} (he : e < d) {p u q : R} (hp : p ∈ (List.map (D M) l1).prod) (hu : u ∈ D M e) (hq : q ∈ (List.map (D M) l2).prod) : p * (u * q) ∈ D M x

Single-stratum version of prod_core.

theorem DGH.prod_sum_mem {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} (hx : x ≠ 0) (hsc : SumClosed (D M x)) {s : Multiset Ordinal.{0}} (hs : s ∈ prodCand (D M) x) (hmin : ∀ t ∈ prodCand (D M) x, ¬t.IsDershowitzMannaLT s) {l1 l2 : List Ordinal.{0}} {d : Ordinal.{0}} (hl : ↑(l1 ++ d :: l2) = s) {p q : R} (hp : p ∈ (List.map (D M) l1).prod) (hq : q ∈ (List.map (D M) l2).prod) (r : Multiset Ordinal.{0}) : (∀ y ∈ r, y < d) → ∀ u ∈ sumSets (D M) r, p * (u * q) ∈ D M x

Distributivity: substituting a sum of strata < d, when D x is closed under sums.

theorem DGH.prod_subst {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : s ∈ prodCand (D M) x) {d : Ordinal.{0}} (hd : d ∈ s) (H : ∀ (l1 l2 : List Ordinal.{0}), ↑(l1 ++ d :: l2) = s → ∀ p ∈ (List.map (D M) l1).prod, ∀ u ∈ D M d, ∀ q ∈ (List.map (D M) l2).prod, p * (u * q) ∈ D M x) : False

Reduction: if every substitution of the factor d lands in D x, s was no candidate.

theorem DGH.prod_entry {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} (hx : x ≠ 0) (hsc : SumClosed (D M x)) {s : Multiset Ordinal.{0}} (hs : s ∈ prodCand (D M) x) (hmin : ∀ t ∈ prodCand (D M) x, ¬t.IsDershowitzMannaLT s) {d : Ordinal.{0}} (hd : d ∈ s) : d = 1 ∨ ∃ (a : Ordinal.{0}), d = Order.succ a ∧ a ≠ 0 ∧ SumClosed (D M a) ∧ MulClosed (D M a) ∧ ¬InvClosed (D M a)

(P1) The entries of the chosen multiset of a product step are 1 or successors of inverse steps.

7. Minimality against Jakobs' order (global form of M1-M3)

theorem DGH.sum_min_jakobs {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : s ∈ sumCand (D M) x) (hmin : ∀ t ∈ sumCand (D M) x, ¬t.IsDershowitzMannaLT s) {t : Multiset Ordinal.{0}} (ht0 : t ≠ 0) (ht : ¬sumSets (D M) t ⊆ D M x) (hts : jakobsLT t s) : False

theorem DGH.prod_min_jakobs {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} {s : Multiset Ordinal.{0}} (hs : s ∈ prodCand (D M) x) (hmin : ∀ t ∈ prodCand (D M) x, ¬t.IsDershowitzMannaLT s) {t : Multiset Ordinal.{0}} (ht0 : t ≠ 0) (ht : ¬prodSets (D M) t ⊆ D M x) (hts : jakobsLT t s) : False

8. Steps, label sets, potentials

def DGH.InvStep {R : Type} [Ring R] (M : Set R) (a : Ordinal.{0}) : Prop

a is an inverse step (case 3) in [1, ε₀).

Equations

• DGH.InvStep M a = (a ≠ 0 ∧ a < Ordinal.epsilon 0 ∧ DGH.SumClosed (DGH.D M a) ∧ DGH.MulClosed (DGH.D M a) ∧ ¬DGH.InvClosed (DGH.D M a))

def DGH.ProdStep {R : Type} [Ring R] (M : Set R) (a : Ordinal.{0}) : Prop

a is a product step (case 2) in [1, ε₀).

Equations

• DGH.ProdStep M a = (a ≠ 0 ∧ a < Ordinal.epsilon 0 ∧ DGH.SumClosed (DGH.D M a) ∧ ¬DGH.MulClosed (DGH.D M a))

def DGH.Qset {R : Type} [Ring R] (M : Set R) : Set Ordinal.{0}

Labels for product steps: 1 and the successors of inverse steps.

Equations

• DGH.Qset M = {d : Ordinal.{0} | d = 1 ∨ ∃ (a : Ordinal.{0}), d = Order.succ a ∧ DGH.InvStep M a}

def DGH.Sset {R : Type} [Ring R] (M : Set R) : Set Ordinal.{0}

Labels for sum steps: 1 and the successors of inverse or product steps.

Equations

• DGH.Sset M = {d : Ordinal.{0} | d = 1 ∨ ∃ (a : Ordinal.{0}), d = Order.succ a ∧ (DGH.InvStep M a ∨ DGH.ProdStep M a)}

def DGH.HInv {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) : Prop

Hypothesis (H_A): every inverse step in [1, ε₀) has a failing index ≤ A.

Equations

• DGH.HInv M A = ∀ (x : Ordinal.{0}), DGH.InvStep M x → ∃ c ≤ A, ¬DGH.invSet (DGH.D M c) ⊆ DGH.D M x

noncomputable def DGH.iota {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : Ordinal.{0}

Inverse potential.

Equations

• DGH.iota M A x = DGH.pot {c : Ordinal.{0} | ¬DGH.invSet (DGH.D M c) ⊆ DGH.D M x} (A + 1)

noncomputable def DGH.piHat {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : Ordinal.{0}

Product potential.

Equations

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

noncomputable def DGH.mu {R : Type} [Ring R] (M : Set R) (A d : Ordinal.{0}) : Ordinal.{0}

Label of sum entries.

Equations

• DGH.mu M A d = DGH.nadd (DGH.iota M A d) (DGH.piHat M A d)

noncomputable def DGH.bnd (A : Ordinal.{0}) : Ordinal.{0}

Bound of mu.

Equations

• DGH.bnd A = DGH.nadd (A + 1) (Ordinal.omega0 ^ (A + 1 + 1))

noncomputable def DGH.sigHat {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : Ordinal.{0}

Sum potential.

Equations

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

noncomputable def DGH.Phi {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : Ordinal.{0}

Total potential.

Equations

• DGH.Phi M A x = DGH.nadd (DGH.mu M A x) (DGH.sigHat M A x)

inverse potential

theorem DGH.iota_mono {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) {x y : Ordinal.{0}} (h : x ≤ y) : iota M A x ≤ iota M A y

theorem DGH.iota_le {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : iota M A x ≤ A + 1

theorem DGH.iota_lt_succ {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) {x : Ordinal.{0}} (hx : InvStep M x) : iota M A x < iota M A (Order.succ x)

theorem DGH.one_le_of_mem_succ_form {d : Ordinal.{0}} (hd : d = 1 ∨ ∃ (a : Ordinal.{0}), d = Order.succ a) : 1 ≤ d

theorem DGH.iota_strictOn {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) {d d' : Ordinal.{0}} (hd : d ∈ Qset M) (hd' : d' ∈ Qset M) (h : d < d') : iota M A d < iota M A d'

product potential

theorem DGH.piHat_mono {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) {x y : Ordinal.{0}} (h : x ≤ y) : piHat M A x ≤ piHat M A y

theorem DGH.piHat_le {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : piHat M A x ≤ Ordinal.omega0 ^ (A + 1 + 1)

theorem DGH.hval_map_iota_lt {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (t : Multiset Ordinal.{0}) : hval (Multiset.map (iota M A) t) < Ordinal.omega0 ^ (A + 1 + 1)

theorem DGH.piHat_lt_succ {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) {x : Ordinal.{0}} (hx : ProdStep M x) : piHat M A x < piHat M A (Order.succ x)

sum labels and sum potential

theorem DGH.mu_mono {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) {x y : Ordinal.{0}} (h : x ≤ y) : mu M A x ≤ mu M A y

theorem DGH.mu_le {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : mu M A x ≤ bnd A

theorem DGH.mu_lt_succ {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) {a : Ordinal.{0}} (ha : InvStep M a ∨ ProdStep M a) : mu M A a < mu M A (Order.succ a)

theorem DGH.mu_strictOn {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) {d d' : Ordinal.{0}} (hd : d ∈ Sset M) (hd' : d' ∈ Sset M) (h : d < d') : mu M A d < mu M A d'

theorem DGH.sigHat_mono {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) {x y : Ordinal.{0}} (h : x ≤ y) : sigHat M A x ≤ sigHat M A y

theorem DGH.sigHat_le {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : sigHat M A x ≤ Ordinal.omega0 ^ (bnd A + 1)

theorem DGH.hval_map_mu_lt {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (t : Multiset Ordinal.{0}) : hval (Multiset.map (mu M A) t) < Ordinal.omega0 ^ (bnd A + 1)

theorem DGH.sigHat_lt_succ {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) {x : Ordinal.{0}} (hx0 : x ≠ 0) (hxe : x < Ordinal.epsilon 0) (h1 : ¬SumClosed (D M x)) : sigHat M A x < sigHat M A (Order.succ x)

total potential

theorem DGH.Phi_mono {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) {x y : Ordinal.{0}} (h : x ≤ y) : Phi M A x ≤ Phi M A y

theorem DGH.Phi_le {R : Type} [Ring R] (M : Set R) (A x : Ordinal.{0}) : Phi M A x ≤ nadd (bnd A) (Ordinal.omega0 ^ (bnd A + 1))

theorem DGH.Phi_lt_succ {R : Type} [Ring R] (M : Set R) (A : Ordinal.{0}) (hA : HInv M A) (H4 : ∀ (x : Ordinal.{0}), x ≠ 0 → x < Ordinal.epsilon 0 → ¬(SumClosed (D M x) ∧ MulClosed (D M x) ∧ InvClosed (D M x))) {x : Ordinal.{0}} (hx0 : x ≠ 0) (hxe : x < Ordinal.epsilon 0) : Phi M A x < Phi M A (Order.succ x)

theorem DGH.main_contra {R : Type} [Ring R] (M : Set R) {A : Ordinal.{0}} (hAe : A < Ordinal.epsilon 0) (H4 : ∀ (x : Ordinal.{0}), x ≠ 0 → x < Ordinal.epsilon 0 → ¬(SumClosed (D M x) ∧ MulClosed (D M x) ∧ InvClosed (D M x))) (hA : HInv M A) : False

Main lemma: (H_A) with A < ε₀ (and no stationary step below ε₀) is impossible.

9. Stationarity and the theorem

theorem DGH.D_stationary {R : Type} [Ring R] (M : Set R) {x : Ordinal.{0}} (hx0 : x ≠ 0) (h1 : SumClosed (D M x)) (h2 : MulClosed (D M x)) (h3 : InvClosed (D M x)) (y : Ordinal.{0}) : x ≤ y → D M y = D M x

Case 4 at x makes the stratification constant from x on.

theorem DGH.epsilon_zero_ne_zero : Ordinal.epsilon 0 ≠ 0

theorem DGH.epsilon_zero_not_succ : ¬∃ (a : Ordinal.{0}), Ordinal.epsilon 0 = Order.succ a

theorem DGH.mem_D_epsilon_zero {R : Type} [Ring R] (M : Set R) {z : R} : z ∈ D M (Ordinal.epsilon 0) ↔ ∃ b < Ordinal.epsilon 0, z ∈ D M b

theorem DGH.kappa_le_epsilon0 {R : Type} [Ring R] (M : Set R) : SumClosed (D M (Ordinal.epsilon 0)) ∧ MulClosed (D M (Ordinal.epsilon 0)) ∧ InvClosed (D M (Ordinal.epsilon 0))

κ ≤ ε₀. For every ring R and every M ⊆ R, the DGH stratum D M ε₀ is closed under sums, products, and inverses of those of its elements that are units of R.