25 states is enough

no 16

merge 16 to 4

Author: lengyijun

GoldbachTm.lean

@@ -4,13 +4,13 @@ import GoldbachTm.Basic
 import GoldbachTm.Format
 import GoldbachTm.ListBlank
 
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.Transition
-import GoldbachTm.Tm26.Miscellaneous
-import GoldbachTm.Tm26.Prime
-import GoldbachTm.Tm26.PBP
-import GoldbachTm.Tm26.Content
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.Transition
+import GoldbachTm.Tm25.Miscellaneous
+import GoldbachTm.Tm25.Prime
+import GoldbachTm.Tm25.PBP
+import GoldbachTm.Tm25.Content
 
 import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.Search0

GoldbachTm/Basic.lean

@@ -129,7 +129,7 @@ induction n with
 
 /-
 P i => nth_cfg i ≠ none
-Q i n => nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+Q i n => nth_cfg i = some ⟨⟨24, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
 -/
 theorem propagating_induction (P : ℕ → Prop) (Q : ℕ → ℕ → Prop)
                (base : ℕ) (hbase : Q base 0)

GoldbachTm/Tm26/Content.lean GoldbachTm/Tm25/Content.lean

@@ -1,20 +1,20 @@
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.PBP
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm26
+namespace Tm25
 
-theorem lemma_22 (n : ℕ) (i : ℕ)
+theorem lemma_21 (n : ℕ) (i : ℕ)
 (even_n : Even (n+2))
 (g :
-nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
+nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
 ( hpp : Goldbach (n+4)) :
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 forward g
 repeat rw [← List.replicate_succ] at g
-apply (leap_18 _ _ 0) at g
+apply (leap_17 _ _ 0) at g
 any_goals omega
 any_goals assumption
 refine (?_ ∘ g) ?_
@@ -40,7 +40,7 @@ refine (?_ ∘ g) ?_
 
 lemma never_halt_step (n : ℕ) :
 (∀ i < n, Goldbach (2*i+4)) ->
-∃ j, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
  := by
 induction n with
 | zero =>
@@ -54,7 +54,7 @@ refine (?_ ∘ induction_step) ?_
 . intros g
   obtain ⟨j, g⟩ := g
   specialize h n (by omega)
-  apply lemma_22 at g
+  apply lemma_21 at g
   . specialize g h
     obtain ⟨k, g⟩ := g
     use k
@@ -73,7 +73,7 @@ apply never_halt_step at IH
 obtain ⟨j, g⟩ := IH
 forward g
 repeat rw [← List.replicate_succ] at g
-apply (leap_18_halt _ _ 0) at g
+apply (leap_17_halt _ _ 0) at g
 any_goals omega
 by_contra! h
 refine (?_ ∘ g) ?_
@@ -88,10 +88,10 @@ refine (?_ ∘ g) ?_
 
 theorem halt_lemma_rev' (h : ∀ n, Goldbach (2*n+4)) :
 ∀ i, nth_cfg i ≠ none := by
-apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
+apply propagating_induction (fun i => nth_cfg i ≠ none) (fun i n => nth_cfg i = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩) 45
 . simp [cfg45]; tauto
 . intros i n g
-  apply (lemma_22 (2*n)) at g
+  apply (lemma_21 (2*n)) at g
   . specialize g (h _)
     obtain ⟨j, g⟩ := g
     use j
@@ -120,7 +120,7 @@ by rw [← Mathlib.Tactic.PushNeg.not_not_eq (Goldbach (2*i+4))]
 )
 forward hj
 repeat rw [← List.replicate_succ] at hj
-apply (leap_18_halt _ _ 0) at hj
+apply (leap_17_halt _ _ 0) at hj
 any_goals omega
 apply hj
 intros x y _
@@ -135,4 +135,4 @@ by_contra! g
 apply halt_lemma_rev' at g
 tauto
 
-end Tm26
+end Tm25

GoldbachTm/Tm26/Miscellaneous.lean GoldbachTm/Tm25/Miscellaneous.lean

@@ -1,9 +1,9 @@
 -- some lemmas tm31 doesn't contain
 
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Transition
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Transition
 
-namespace Tm26
+namespace Tm25
 
 theorem lemma7 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨7, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
@@ -39,7 +39,7 @@ induction k with (intros i l r h; simp_all)
 
 theorem lemma5 (k : ℕ): ∀ (i : ℕ) (l r : List Γ),
 nth_cfg i = some ⟨⟨5, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate k Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk r⟩⟩ →
-nth_cfg (i + k + 2) = some ⟨⟨4, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
+nth_cfg (i + k + 2) = some ⟨⟨7, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (Γ.zero :: l), Turing.ListBlank.mk (List.replicate k Γ.zero ++ r)⟩⟩ := by
 induction k with (intros i l r h; simp_all)
 | zero => iterate 2 forward h
           rw [← h]
@@ -111,4 +111,4 @@ cases r1 with simp_all
              simp [h]
              omega
 
-end Tm26
+end Tm25

GoldbachTm/Tm26/PBP.lean GoldbachTm/Tm25/PBP.lean

@@ -1,24 +1,24 @@
 -- PDP is short for "prime board prime"
-import GoldbachTm.Tm26.TuringMachine26
-import GoldbachTm.Tm26.Search0
-import GoldbachTm.Tm26.Prime
+import GoldbachTm.Tm25.TuringMachine25
+import GoldbachTm.Tm25.Search0
+import GoldbachTm.Tm25.Prime
 import Mathlib.Data.Nat.Prime.Defs
 
-namespace Tm26
+namespace Tm25
 
 -- l1 : count of 1 on the left
 -- r1 : count of 1 on the right
-theorem lemma_18 (i l1 r1: ℕ)
+theorem lemma_17 (i l1 r1: ℕ)
 (hp : ¬ Nat.Prime (l1+1) \/ ¬ Nat.Prime (r1+1))
 (g :
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
 ):
-∃ j>i, nth_cfg j = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one), Turing.ListBlank.mk (List.replicate (r1+2) Γ.one)⟩⟩ := by
+∃ j>i, nth_cfg j = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one), Turing.ListBlank.mk (List.replicate (r1+2) Γ.one)⟩⟩ := by
 forward g
 forward g
 forward g
 by_cases hr1 : Nat.Prime (r1+1)
-. refine (?_ ∘ (prime_21 (3+i) r1 (Γ.one :: List.replicate l1 Γ.one) [])) ?_
+. refine (?_ ∘ (prime_20 (3+i) r1 (Γ.one :: List.replicate l1 Γ.one) [])) ?_
   . intros g
     specialize g hr1
     obtain ⟨j, _, g⟩ := g
@@ -30,18 +30,18 @@ by_cases hr1 : Nat.Prime (r1+1)
       use 1
       tauto
     rw [h] at g
-    apply (rec24 l1 (1+j) []) at g
+    apply (rec23 l1 (1+j) []) at g
     forward g
     have h : ¬ Nat.Prime (l1+1) := by tauto
-    apply n_prime_17 at h
+    apply n_prime_16 at h
     pick_goal 5
     . rw [g]
       simp
       repeat any_goals apply And.intro
       all_goals rfl
     obtain ⟨m, _, h⟩ := h
     iterate 3 forward h
-    apply rec22 at h
+    apply rec21 at h
     forward h
     use (5+m+l1)
     constructor
@@ -61,7 +61,7 @@ by_cases hr1 : Nat.Prime (r1+1)
     left
     use 1
     tauto
-. apply n_prime_17 at hr1
+. apply n_prime_16 at hr1
   pick_goal 5
   . rw [g]
     simp
@@ -95,13 +95,13 @@ theorem both_prime (i l1 r1: ℕ)
 (hpr : Nat.Prime (r1+1))
 (even_sum : Even (l1+r1))
 (g :
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
 ) :
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩ := by
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩ := by
 forward g
 forward g
 forward g
-apply prime_21 at hpr
+apply prime_20 at hpr
 pick_goal 5
 . rw [g]
   simp
@@ -122,9 +122,9 @@ have h : Turing.ListBlank.mk (List.replicate l1 Γ.one) = Turing.ListBlank.mk (L
   use 1
   tauto
 rw [h] at g
-apply (rec24 l1 (1+j) []) at g
+apply (rec23 l1 (1+j) []) at g
 forward g
-apply prime_21 at hpl
+apply prime_20 at hpl
 pick_goal 5
 . rw [g]
   simp
@@ -133,15 +133,15 @@ obtain ⟨m, _, g⟩ := hpl
 forward g
 forward g
 forward g
-apply rec23 at g
+apply rec22 at g
 forward g
 rw [← List.cons_append] at g
 rw [← List.replicate_succ] at g
 rw [← List.cons_append] at g
 rw [← List.replicate_succ] at g
 rw [List.append_cons] at g
 rw [← List.replicate_succ'] at g
-apply rec24 at g
+apply rec23 at g
 forward g
 rw [← List.cons_append] at g
 rw [← List.replicate_succ] at g
@@ -151,7 +151,7 @@ rw [List.append_cons] at g
 rw [← List.replicate_succ'] at g
 rw [← List.append_assoc] at g
 rw [← List.replicate_add] at g
-apply n_prime_17 at g
+apply n_prime_16 at g
 refine (?_ ∘ g) ?_
 . clear g
   intros g
@@ -161,7 +161,7 @@ refine (?_ ∘ g) ?_
   forward g
   rw [← List.cons_append] at g
   rw [← List.replicate_succ] at g
-  apply rec22 at g
+  apply rec21 at g
   use (3 + n + (2 + l1 + r1 + 1) + 1)
   constructor
   . omega
@@ -182,20 +182,20 @@ refine (?_ ∘ g) ?_
     assumption
 
 
-theorem leap_18 (l1 : ℕ) : ∀ (i r1: ℕ),
+theorem leap_17 (l1 : ℕ) : ∀ (i r1: ℕ),
 l1 + r1 ≥ 2 →
 Even (l1+r1) →
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
 (∃ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y /\ (r1+1) ≤ x /\ x ≤ y) →
-∃ j>i, nth_cfg j = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+∃ j>i, nth_cfg j = some ⟨⟨21, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 induction l1 with
 | zero => omega
 | succ l1 induction_step =>
   intros i r1 h _ g hpp
   by_cases hp : ¬ Nat.Prime (l1+2) \/ ¬ Nat.Prime (r1+1)
   . -- induction step
-    apply lemma_18 at g
+    apply lemma_17 at g
     any_goals tauto
     obtain ⟨j, _, g⟩ := g
     apply induction_step at g
@@ -231,9 +231,9 @@ induction l1 with
     all_goals tauto
 
 
-theorem leap_18_halt (l1 : ℕ) : ∀ (i r1: ℕ),
+theorem leap_17_halt (l1 : ℕ) : ∀ (i r1: ℕ),
 l1 + r1 ≥ 2 →
-nth_cfg i = some ⟨⟨18, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
+nth_cfg i = some ⟨⟨17, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩ →
 (∀ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y → False) →
 ∃ j, nth_cfg j = none
 := by
@@ -249,7 +249,7 @@ induction l1 with
   rw [← List.replicate_succ] at g
   rw [← List.replicate_succ] at g
   by_cases hp : Nat.Prime (r2+3)
-  . apply prime_21 at hp
+  . apply prime_20 at hp
     pick_goal 5
     . rw [g]
       simp
@@ -263,7 +263,7 @@ induction l1 with
     obtain ⟨j, _, h⟩ := hp
     iterate 13 forward h
     use (13+j)
-  . apply n_prime_17 at hp
+  . apply n_prime_16 at hp
     pick_goal 5
     . rw [g]
       simp
@@ -279,7 +279,7 @@ induction l1 with
     use (3+j)
 | succ l1 induction_step =>
     intros i r1 h g hpp
-    apply lemma_18 at g
+    apply lemma_17 at g
     . obtain ⟨j, _, g⟩ := g
       apply induction_step at g
       any_goals omega
@@ -293,4 +293,4 @@ induction l1 with
       ring_nf
       tauto
 
-end Tm26
+end Tm25