Show that if a semigroup is not anomalous, then it has large elements

OrderedSemigroups/Archimedean.lean

@@ -380,6 +380,10 @@ theorem not_anomalous_comm_and_arch (not_anomalous : ¬has_anomalous_pair (α :=
   · have := mt (non_archimedean_anomalous_pair (α := α)) not_anomalous
     simpa
 
+def not_anomalous_comm_semigroup (not_anomalous : ¬has_anomalous_pair (α := α)) :
+    LinearOrderedCancelCommSemigroup α where
+  mul_comm a b := not_anomalous_pair_commutative not_anomalous a b
+
 theorem lt_not_anomalous_difference {a b : α} (h : a < b) (not_anomalous : ¬has_anomalous_pair (α := α)) :
     ∃n : ℕ+, a^(n+1) ≤ b^n := by
   by_contra hx
@@ -531,4 +535,114 @@ theorem not_anomalous_iff_large_difference : ¬has_anomalous_pair (α := α) ↔
   · exact fun a ↦ not_anomalous_large_difference a
   · exact fun a ↦ large_difference_not_anomalous a
 
+theorem pos_large_elements (not_anomalous : ¬has_anomalous_pair (α := α)) (pos_elem : ∃a : α, is_positive a) :
+    ∀x : α, ∃y : α, is_positive y ∧ is_positive (x*y) := by
+  intro x
+  obtain ⟨z, hz⟩ := pos_elem
+  obtain pos_x | neg_x | one_x := pos_neg_or_one x
+  -- If `x` is positive we're immediately done
+  · use x
+    constructor
+    · trivial
+    · exact pos_sq_pos pos_x
+  -- `x` is negative
+  · by_contra! all_pos_small
+    have xzn2_negative (n : ℕ+) : is_negative (x * z^(n+2)) := by
+      have zn2_lt_zn3 : z^(n+2) < z^(n+3) := by
+        calc z^(n+3)
+        _ = z^(n+2)*z := ppow_succ (n + 2) z
+        _ > z^(n+2) := pos_right hz (z ^ (n + 2))
+      have  xzn3_lt_xzn3 : x*z^(n+2) < x*z^(n+3) := mul_lt_mul_left' zn2_lt_zn3 x
+      have : is_positive (z^(n+3)) := pos_pow_pos hz (n + 3)
+      have zn3_not_pos := all_pos_small (z^(n+3)) this
+      rw [not_pos_or] at zn3_not_pos
+      obtain zn3_neg | zn3_one := zn3_not_pos
+      · exact lt_neg_neg zn3_neg xzn3_lt_xzn3
+      · exact lt_one_neg zn3_one xzn3_lt_xzn3
+    have : has_anomalous_pair (α := α) := by
+      simp [has_anomalous_pair]
+      use x*z, x
+      simp [anomalous_pair]
+      intro n
+      right
+      obtain ⟨is_comm, _⟩ := not_anomalous_comm_and_arch not_anomalous
+      constructor
+      · have : (x*z)^n = x^n * z^n := mul_pow_comm_semigroup is_comm x z n
+        rw [this]
+        have : is_positive (z^n) := pos_pow_pos hz n
+        exact pos_right this (x ^ n)
+      · have := xzn2_negative n
+        calc x^n
+        _ > x^n*(x*z^(n+2)) := neg_right (xzn2_negative n) (x ^ n)
+        _ = (x^n*x)*(z^(n+2)) := by simp [mul_assoc]
+        _ = x^(n+1) * (z^(n+2)) := by simp [ppow_succ]
+        _ = x^(n+1) * (z^(n+1) * z) := by
+          have : n+2 = (n+1)+1 := rfl
+          simp [this, ppow_succ]
+        _ = x^(n+1) * z^(n+1) * z := by simp [mul_assoc]
+        _ = (x * z)^(n+1) * z := by simp [mul_pow_comm_semigroup is_comm]
+        _ > (x * z)^(n+1) := pos_right hz ((x * z) ^ (n + 1))
+    contradiction
+  -- If `x` is one, we're immediately done
+  · use z
+    constructor
+    · trivial
+    · have : x * z = z := one_x z
+      simpa [this]
+
+theorem neg_large_elements (not_anomalous : ¬has_anomalous_pair (α := α)) (neg_elem : ∃a : α, is_negative a) :
+    ∀x : α, ∃y : α, is_negative y ∧ is_negative (x*y) := by
+  intro x
+  obtain ⟨z, hz⟩ := neg_elem
+  obtain pos_x | neg_x | one_x := pos_neg_or_one x
+  -- `x` is positive
+  · by_contra! all_neg_small
+    have xzn2_positive (n : ℕ+) : is_positive (x * z^(n+2)) := by
+      have zn2_gt_zn3 : z^(n+2) > z^(n+3) := by
+        calc z^(n+3)
+        _ = z^(n+2)*z := ppow_succ (n + 2) z
+        _ < z^(n+2) := neg_right hz (z ^ (n + 2))
+      have  xzn3_lt_xzn3 : x*z^(n+2) > x*z^(n+3) := mul_lt_mul_left' zn2_gt_zn3 x
+      have : is_negative (z^(n+3)) := neg_pow_neg hz (n + 3)
+      have zn3_not_neg := all_neg_small (z^(n+3)) this
+      rw [not_neg_or] at zn3_not_neg
+      obtain zn3_pos | zn3_one := zn3_not_neg
+      · exact pos_lt_pos zn3_pos xzn3_lt_xzn3
+      · exact gt_one_pos zn3_one xzn3_lt_xzn3
+    have : has_anomalous_pair (α := α) := by
+      simp [has_anomalous_pair]
+      use x*z, x
+      simp [anomalous_pair]
+      intro n
+      left
+      obtain ⟨is_comm, _⟩ := not_anomalous_comm_and_arch not_anomalous
+      constructor
+      · have : (x*z)^n = x^n * z^n := mul_pow_comm_semigroup is_comm x z n
+        rw [this]
+        have : is_negative (z^n) := neg_pow_neg hz n
+        exact neg_right this (x ^ n)
+      · have := xzn2_positive n
+        calc x^n
+        _ < x^n*(x*z^(n+2)) := pos_right (xzn2_positive n) (x ^ n)
+        _ = (x^n*x)*(z^(n+2)) := by simp [mul_assoc]
+        _ = x^(n+1) * (z^(n+2)) := by simp [ppow_succ]
+        _ = x^(n+1) * (z^(n+1) * z) := by
+          have : n+2 = (n+1)+1 := rfl
+          simp [this, ppow_succ]
+        _ = x^(n+1) * z^(n+1) * z := by simp [mul_assoc]
+        _ = (x * z)^(n+1) * z := by simp [mul_pow_comm_semigroup is_comm]
+        _ < (x * z)^(n+1) := neg_right hz ((x * z) ^ (n + 1))
+    contradiction
+  -- If `x` is negative, we're immediately done
+  · use x
+    constructor
+    · trivial
+    · exact product_of_neg_neg neg_x
+  -- If `x` is one, we're immediately done
+  · use z
+    constructor
+    · trivial
+    · have : x * z = z := one_x z
+      simpa [this]
+
 end LinearOrderedCancelSemigroup

OrderedSemigroups/Basic.lean

@@ -15,7 +15,7 @@ variable {α : Type u}
 section Semigroup'
 variable [Semigroup' α]
 
-theorem nppow_eq_nppowRec : Semigroup'.nppow = nppowRec (α := α) := by
+theorem nppow_eq_nppowRec : Semigroup'.nppow = nppowRec (α := α):= by
   ext x y
   induction x using PNat.recOn with
   | p1 => simp [Semigroup'.nppow_one, nppowRec_one]
@@ -68,6 +68,16 @@ theorem split_first_and_last_factor_of_product {a b : α} {n : ℕ+} :
       _                   = a * ((b*a)^n * (b*a)) * b := by simp [mul_assoc]
       _                   = a * (b*a)^(n+1) * b := by rw [←ppow_succ]
 
+theorem mul_pow_comm_semigroup (is_comm : ∀x y : α, x * y = y * x)
+    (a b : α) (n : ℕ+) : (a*b)^n = a^n * b^n := by
+  induction n using PNat.recOn with
+  | p1 => simp
+  | hp n ih =>
+    simp [ppow_succ, ih]
+    calc a ^ n * b ^ n * (a * b)
+    _ = a ^ n * (b ^ n * a) * b := by simp [mul_assoc]
+    _ = a ^ n * (a * b ^ n) * b := by simp [is_comm]
+    _ = a ^ n * a * (b ^ n * b) := by simp [mul_assoc]
 end Semigroup'
 
 section OrderedSemigroup

OrderedSemigroups/Defs.lean

@@ -57,6 +57,8 @@ class Semigroup' (α : Type u) extends Semigroup α where
   nppow_one : ∀ x, nppow 1 x = x := by intros x; exact nppowRec_one x
   nppow_succ : ∀ (n : ℕ+) (x), nppow (n+1) x = nppow n x * x := by intros x; exact nppowRec_succ x
 
+instance {β : Type*} [Semigroup β] : Semigroup' β where
+
 /-- Define the exponentiation notation for the action of ℕ+ on a semigroup' -/
 instance [Semigroup' α] : Pow α ℕ+ :=
   ⟨fun x n ↦ Semigroup'.nppow n x⟩
@@ -109,7 +111,7 @@ instance [LinearOrderedCancelSemigroup α] : LinearOrderedSemigroup α where
   max_def := LinearOrderedCancelSemigroup.max_def
   compare_eq_compareOfLessAndEq := LinearOrderedCancelSemigroup.compare_eq_compareOfLessAndEq
 
-class CommSemigroup' (G : Type u) extends Semigroup' G, CommMagma G where
+class CommSemigroup' (G : Type u) extends Semigroup' G, CommSemigroup G where
 
 class LinearOrderedCancelCommSemigroup (α : Type u) extends LinearOrderedCancelSemigroup α, CommSemigroup' α where
 

OrderedSemigroups/Sign.lean

@@ -50,6 +50,12 @@ theorem one_not_neg {a : α} (is_zer : is_one a) : ¬is_negative a := by
   rw [is_zer a] at is_neg
   exact (lt_self_iff_false a).mp is_neg
 
+theorem pos_sq_pos {a : α} (is_pos : is_positive a) : is_positive (a*a) := by
+  simp [is_positive]
+  intro x
+  have := gt_trans (is_pos (a * x)) (is_pos x)
+  simpa [mul_assoc]
+
 /-
 theorem pos_le_pos {a b : α} (pos : is_positive a) (h : a ≤ b) : is_positive b :=
   fun x ↦ lt_mul_of_lt_mul_right (pos x) h
@@ -158,9 +164,15 @@ variable [OrderedSemigroup α]
 theorem pos_le_pos {a b : α} (pos : is_positive a) (h : a ≤ b) : is_positive b :=
   fun x ↦ lt_mul_of_lt_mul_right (pos x) h
 
+theorem pos_lt_pos {a b : α} (pos : is_positive a) (h : a < b) : is_positive b :=
+  pos_le_pos pos h.le
+
 theorem le_neg_neg {a b : α} (neg : is_negative a) (h : b ≤ a) : is_negative b :=
   fun x ↦ mul_lt_of_mul_lt_right (neg x) h
 
+theorem lt_neg_neg {a b : α} (neg : is_negative a) (h : b < a) : is_negative b :=
+  le_neg_neg neg h.le
+
 end OrderedSemigroup
 
 section LinearOrderedCancelSemigroup