lemma_26

GoldbachTm/Tm31/PBP.lean

@@ -1,12 +1,110 @@
 -- PDP is short for "prime board prime"
 import GoldbachTm.Tm31.TuringMachine31
+import GoldbachTm.Tm31.Search0
+import GoldbachTm.Tm31.Prime
 import Mathlib.Data.Nat.Prime.Defs
 
--- TODO: maybe need double 0
 -- l1 : count of 1 on the left
 -- r1 : count of 1 on the right
-theorem lemma_26 : ∀ (i l1 r1: ℕ) (l r : List Γ),
-nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ →
-(¬ Nat.Prime (l1+1)) \/ (¬ Nat.Prime r1) →
-∃ j, nth_cfg (i+j) = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one ++ List.cons Γ.zero l), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
-sorry
+theorem lemma_26 (i l1 r1: ℕ)
+(hp : ¬ Nat.Prime (l1+1) \/ ¬ Nat.Prime (r1+1))
+(g :
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate (r1+1) Γ.one)⟩⟩
+):
+∃ j, nth_cfg (i+j) = some ⟨⟨28, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate l1 Γ.one), Turing.ListBlank.mk (List.replicate (r1+2) Γ.one)⟩⟩ := by
+forward g g i
+by_cases hr1 : Nat.Prime (r1+1)
+. refine (?_ ∘ (lemma_23 (1+i) r1 (Γ.one :: List.replicate l1 Γ.one) [])) ?_
+  . intros g
+    specialize g hr1
+    obtain ⟨j, g⟩ := g
+    forward g g (1+i+j)
+    refine (?_ ∘ (lemma_23_to_27 (2+i+j) l1 [] (Γ.zero :: Γ.one :: (List.replicate r1 Γ.one ++ [Γ.zero])))) ?_
+    . intros g
+      obtain ⟨k, g⟩ := g
+      forward g g (k+(2+i+j))
+      have h : ¬ Nat.Prime (l1+1) := by tauto
+      apply lemma_not_prime at h
+      pick_goal 5
+      . rw [g]
+        simp
+        repeat any_goals apply And.intro
+        all_goals rfl
+      obtain ⟨m, h⟩ := h
+      forward h h (3+k+i+j+m)
+      forward h h (4+k+i+j+m)
+      forward h h (5+k+i+j+m)
+      apply rec30 at h
+      forward h h (6+k+i+j+m+l1+1)
+      use (8+k+j+m+l1)
+      ring_nf at *
+      simp [h]
+      repeat any_goals apply And.intro
+      all_goals simp! [Turing.ListBlank.mk]
+      all_goals rw [Quotient.eq'']
+      all_goals right
+      . use 2
+        tauto
+      . use 1
+        simp
+        rw [← List.cons_append]
+        rw [← List.cons_append]
+        rw [← List.replicate_succ]
+        rw [← List.replicate_succ]
+        ring_nf
+        tauto
+    . simp! [g, Turing.ListBlank.mk]
+      rw [Quotient.eq'']
+      left
+      use 1
+      tauto
+  . simp! [g, Turing.ListBlank.mk]
+    rw [Quotient.eq'']
+    left
+    use 1
+    tauto
+. apply lemma_not_prime at hr1
+  pick_goal 5
+  . rw [g]
+    simp
+    repeat any_goals apply And.intro
+    . rfl
+    . simp! [Turing.ListBlank.mk]
+      rw [Quotient.eq'']
+      left
+      use 1
+      tauto
+  obtain ⟨j, g⟩ := hr1
+  forward g g (1+i+j)
+  forward g g (2+i+j)
+  forward g g (3+i+j)
+  use (4+j)
+  ring_nf at *
+  simp! [g]
+  simp! [Turing.ListBlank.mk]
+  rw [Quotient.eq'']
+  right
+  use 1
+  rw [← List.cons_append]
+  rw [← List.replicate_succ]
+  rw [← List.cons_append]
+  rw [← List.replicate_succ]
+  ring_nf
+  tauto
+
+-- r1 > 0
+theorem leap_26 (l1 : ℕ) : ∀ (i r1: ℕ),
+l1 + r1 + 1 ≥ 4 /\
+nth_cfg i = some ⟨⟨26, by omega⟩, ⟨Γ.one, Turing.ListBlank.mk (List.replicate (l1+1) Γ.one), Turing.ListBlank.mk (List.replicate r1 Γ.one)⟩⟩ →
+(∃ x y, x + y = l1 + r1 + 1 /\ Nat.Prime x /\ Nat.Prime y /\ r1 ≤ x /\ x ≤ y) →
+∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+3) Γ.one), Turing.ListBlank.mk []⟩⟩
+:= by
+induction l1 with
+| zero => simp
+          intros i r1 _ g x y _ _ _ _ _
+          omega
+| succ l1 =>
+  intros i r1 h _
+  obtain ⟨h, g⟩ := h
+  forward g g i
+  sorry