lemma_25

Author: lengyijun

GoldbachTm/Tm31/Content.lean

@@ -1,12 +1,36 @@
 import GoldbachTm.Tm31.TuringMachine31
+import GoldbachTm.Tm31.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
-theorem lemma_25 (n : ℕ): ∀ (i : ℕ),
-nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate n Γ.one), Turing.ListBlank.mk []⟩⟩ →
-(∃ x y, x + y = n /\ Nat.Prime x /\ Nat.Prime y) →
-∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+theorem lemma_25 (n : ℕ) (i : ℕ)
+(g :
+nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4) Γ.one), Turing.ListBlank.mk []⟩⟩ )
+( hpp : (∃ x y, x + y = n+4 /\ Nat.Prime x /\ Nat.Prime y)) :
+∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
-sorry
+forward g g i
+repeat rw [← List.replicate_succ] at g
+apply (leap_26 _ _ 0) at g
+any_goals omega
+refine (?_ ∘ g) ?_
+. intros g
+  obtain ⟨k, h⟩ := g
+  use (1+k)
+  ring_nf at *
+  simp [h]
+. obtain ⟨x, y, _, hx, hy⟩ := hpp
+  by_cases x ≤ y
+  . use! x, y
+    repeat any_goals apply And.intro
+    any_goals assumption
+    apply Nat.Prime.two_le at hx
+    omega
+  . use! y, x
+    repeat any_goals apply And.intro
+    any_goals assumption
+    any_goals omega
+    apply Nat.Prime.two_le at hy
+    omega
 
 theorem halt_lemma :
 (∃ (n x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y) →