wip

PBP

rename

GoldbachTm.lean

@@ -5,4 +5,7 @@ import GoldbachTm.Format
 import GoldbachTm.ListBlank
 import GoldbachTm.Tm27.TuringMachine27
 import GoldbachTm.Tm31.TuringMachine31
-import GoldbachTm.Tm31.Hello
+import GoldbachTm.Tm31.Search0
+import GoldbachTm.Tm31.Content
+import GoldbachTm.Tm31.Prime
+import GoldbachTm.Tm31.PBP

GoldbachTm/Tm31/Content.lean

@@ -0,0 +1,21 @@
+import GoldbachTm.Tm31.TuringMachine31
+import Mathlib.Data.Nat.Prime.Defs
+
+theorem lemma_25 (k : ℕ): ∀ (i : ℕ),
+nth_cfg i = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate k Γ.one), Turing.ListBlank.mk []⟩⟩ →
+(¬ (∃ x y, x + y = k /\ Nat.Prime x /\ Nat.Prime y)) →
+∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (k+2) Γ.one), Turing.ListBlank.mk []⟩⟩
+:= by
+sorry
+
+theorem halt_lemma :
+(∃ (k x y: ℕ), k % 2 = 0 /\ k >= 4 /\ x + y = k /\ Nat.Prime x /\ Nat.Prime y) →
+∃ i, nth_cfg i = none
+:= by
+sorry
+
+theorem halt_lemma_rev :
+∃ i, nth_cfg i = none →
+(∃ (k x y: ℕ), k % 2 = 0 /\ x + y = k /\ Nat.Prime x /\ Nat.Prime y)
+:= by
+sorry

GoldbachTm/Tm31/PBP.lean

@@ -0,0 +1,12 @@
+-- PDP is short for "prime board prime"
+import GoldbachTm.Tm31.TuringMachine31
+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

GoldbachTm/Tm31/Prime.lean

@@ -0,0 +1,31 @@
+-- theorem of subroutine: judge prime
+
+import GoldbachTm.Tm31.TuringMachine31
+import Mathlib.Data.Nat.Prime.Defs
+
+-- r1 : count of 1 on the right
+theorem lemma_23 : ∀ (i r1: ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨0, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ →
+Nat.Prime r1 →
+∃ j, nth_cfg (i+j) = some ⟨⟨22, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk l, Turing.ListBlank.mk (List.replicate r1 Γ.one ++ List.cons Γ.zero r)⟩⟩ :=
+sorry
+
+--    l 0 [la 11] 0 [lb 1]  0 [ra 11111] 0 [(rb+1) 1] 0 r
+--                          ^
+--
+--    l 0 [la' 1] 0 [lb' 1] 0 [(ra+1) 1] 0 [rb 11111] 0 r
+--                          ^
+theorem lemma_12 : ∀ (i la lb ra rb: ℕ) (l r : List Γ),
+nth_cfg i = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
+  Turing.ListBlank.mk (List.replicate lb Γ.one ++ List.cons Γ.zero (List.replicate la Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate ra Γ.one ++ List.cons Γ.zero (List.replicate (rb+1) Γ.one ++ List.cons Γ.zero r))⟩⟩ →
+  (ra + 2) % (la + lb + 1) = (la + 1) →
+  Nat.Prime r1 →
+∃ j la' lb', nth_cfg (i+j) = some ⟨⟨12, by omega⟩, ⟨Γ.zero,
+  Turing.ListBlank.mk (List.replicate lb' Γ.one ++ List.cons Γ.zero (List.replicate la' Γ.one ++ List.cons Γ.zero l)),
+  Turing.ListBlank.mk (List.replicate (ra+1) Γ.one ++ List.cons Γ.zero (List.replicate rb Γ.one ++ List.cons Γ.zero r))⟩⟩
+  /\ (ra + 3) % (la + lb + 1) = (la' + 1)
+  /\ la + lb = la' + lb'
+:= by
+-- 只要反复 forward 就好了
+sorry

GoldbachTm/Tm31/Hello.lean → GoldbachTm/Tm31/Search0.lean

@@ -1,4 +1,5 @@
 -- theorem of recursive states
+-- all these states' usage is to search 0
 import GoldbachTm.Tm31.TuringMachine31