stuckatpower

UFT/Axioms.lean

@@ -1,4 +1,4 @@
-import Mathlib.Data.Int.LeastGreatest
+import Mathlib.Data.Set.Lattice
 
 structure myRing (α : Type) where
   add : α → α → α
@@ -42,117 +42,3 @@ def myOrderedRing.ge {α : Type} (R : myOrderedRing α) (a b : α) : Prop := --
 structure WellOrderedRing (α : Type) extends myOrderedRing α where
   well_ordered : ∀ (S : Set α), S.Nonempty → S ⊆ tomyOrderedRing.P →
   ∃ m ∈ S, ∀ s ∈ S, myOrderedRing.le tomyOrderedRing s m
-
--- Define the integer ring
-def intRing : myRing Int :={
-  add := Int.add,
-  mul := Int.mul,
-  zero := 0,
-  one := 1,
-  neg := Int.neg,
-  add_comm := Int.add_comm,
-  mul_comm := Int.mul_comm,
-  add_assoc := Int.add_assoc,
-  mul_assoc := Int.mul_assoc,
-  distrib := Int.mul_add,
-  add_zero := Int.add_zero,
-  add_inv := Int.add_right_neg,
-  mul_ident := Int.mul_one
-}
-
-def intP : Set Int :=
-  {x | x > 0}
-
-def orderedIntRing : myOrderedRing Int := {
-  tomyRing := intRing,
-  P := intP,
-  P_nonempty := ⟨1, by simp [intP]⟩,
-  P_add := by
-    intro a b ha hb
-    simp [intP] at *
-    exact Int.add_pos ha hb
-
-  P_mul := by
-    intro a b ha hb
-    simp [intP] at *
-    exact Int.mul_pos ha hb
-
-  trichotomy1 := by
-    simp [intP]
-    exact Int.zero_lt_one
-
-  trichotomy2 := by
-    intro a ha
-    simp [intP] at *
-    have ha' : -a < 0 := by
-      exact Int.neg_neg_of_pos ha
-    exact Int.le_of_lt ha'
-
-  trichotomy3 := by
-    intro a ha hza
-    simp [intP] at *
-    have hza' : 0 ≠ a := by
-      rw [ne_comm]
-      exact hza
-    have h : a < 0 := by
-      exact lt_of_le_of_ne' ha hza'
-    apply Int.neg_pos_of_neg
-    exact h
-}
-
-def wellOrderedIntRing : WellOrderedRing Int := {
-  tomyOrderedRing := orderedIntRing,
-  well_ordered := by
-    intro S hS hP
-
-    have Hinh : ∃ (z : ℤ), z ∈ S := by
-      exact hS
-
-    have Hbdd : ∃ (b : ℤ), ∀ (z : ℤ), z ∈ S → b ≤ z := ⟨0, by
-      intro z hz
-      have z_pos : z ∈ orderedIntRing.P := by
-        exact hP hz
-      have zero_le_pos : ∀ z ∈ orderedIntRing.P, 0 ≤ z := by
-        intro z' hzP
-        simp [intP] at hzP
-        exact Int.le_of_lt hzP
-      exact zero_le_pos z z_pos
-    ⟩
-
-    obtain ⟨lb, lb_in_S, is_least⟩ := Int.exists_least_of_bdd Hbdd Hinh
-    use lb
-    apply And.intro
-    · exact lb_in_S
-
-    intro s s_in_S
-    unfold myOrderedRing.le
-    have Hle := is_least s s_in_S
-    by_cases h_eq : lb = s
-    · right
-      exact h_eq.symm
-    left
-    have Hlt : lb < s := by
-      exact lt_of_le_of_ne Hle h_eq
-
-    have tmp : orderedIntRing.P = intP := by
-      rfl
-    rw [tmp]
-    simp [intP]
-
-    have tmp2 : orderedIntRing.neg = Int.neg := by
-      rfl
-    rw [tmp2]
-
-    have tmp3 : orderedIntRing.add = Int.add := by
-      rfl
-    rw [tmp3]
-
-    simp
-
-    have tmp4 : lb.neg = -lb := by
-      rfl
-    rw [tmp4]
-
-    simp
-    exact Hlt
-}

UFT/PrimeFactorization.lean → UFT/PrimeFactorizationExists.lean

@@ -13,13 +13,6 @@ def is_prime_factorization {α : Type} (R : WellOrderedRing α) (n : α) (factor
     (∀ p ∈ factors, prime R p) ∧
     (list_product R factors = n)
 
-def unique_prime_factorization {α : Type} (R : WellOrderedRing α) (n : α) : Prop :=
-  ∀ (factors1 factors2 : List α),
-    is_prime_factorization R n factors1 →
-    is_prime_factorization R n factors2 →
-    ∃ (perm : List α → List α),
-      perm factors1 = factors2
-
 lemma prime_have_prime_factorization {α : Type} (R : WellOrderedRing α) (p : α) (pprime : prime R p) : is_prime_factorization R p [p] := by
   unfold is_prime_factorization
   constructor

UFT/PrimePowers.lean

@@ -0,0 +1,12 @@
+import UFT.Axioms
+import UFT.RingResults
+import UFT.OrderedRingResults
+import UFT.IntegralDomain
+import UFT.Division
+import UFT.GCD
+import UFT.EuclidsLemma
+
+def power {α : Type} (R : WellOrderedRing α) (base : α) : α → α
+  | exp =>
+    if exp = R.zero then R.one  -- Base case: exponent is zero
+    else R.mul base (power R base (R.sub exp R.one))  -- Recursive case

UFT/UniquePrimeFactorization.lean

@@ -0,0 +1,31 @@
+import UFT.Axioms
+import UFT.RingResults
+import UFT.OrderedRingResults
+import UFT.IntegralDomain
+import UFT.Division
+import UFT.GCD
+import UFT.EuclidsLemma
+import UFT.PrimeFactorizationExists
+
+lemma prime_div_prime_implies_equality {α : Type} (R : WellOrderedRing α) (p : α) (q : α)
+    (hp : prime R p) (hq : prime R q) (hdiv : divisible R p q) : p = q := by
+  unfold prime at *
+  rcases hp with ⟨pgt1, pprime⟩
+  rcases hq with ⟨qgt1, qprime⟩
+  unfold divisible at hdiv
+  rcases hdiv with ⟨r, req⟩
+  have p_gt0 := gt_transitive R.tomyOrderedRing p R.one R.zero pgt1 (one_gt_zero R.tomyOrderedRing)
+  have p_pos := gt0_implies_pos R.tomyOrderedRing p p_gt0
+  have q_pos := gt0_implies_pos R.tomyOrderedRing q (gt_transitive R.tomyOrderedRing q R.one R.zero qgt1 (one_gt_zero R.tomyOrderedRing))
+  have r_pos := pos_a_mul_b_eq_pos_c R.tomyOrderedRing p r q p_pos  q_pos req
+  have r_gt0 := pos_implies_gt0 R.tomyOrderedRing r r_pos
+  have p1_or_r1 := qprime p r req p_gt0 r_gt0
+  rcases p1_or_r1 with (p1 | r1)
+  · rw [p1] at pgt1
+    unfold myOrderedRing.gt at pgt1
+    rw [R.add_inv] at pgt1
+    have zero_npos := R.trichotomy1
+    contradiction
+  · rw [r1] at req
+    rw [R.mul_ident] at req
+    exact req