never_halt

GoldbachTm/Tm31/Content.lean

@@ -2,10 +2,12 @@ import GoldbachTm.Tm31.TuringMachine31
 import GoldbachTm.Tm31.PBP
 import Mathlib.Data.Nat.Prime.Defs
 
+def goldbach (n : ℕ) := ∃ (x y: ℕ), x + y = n /\ Nat.Prime x /\ Nat.Prime y
+
 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)) :
+( hpp : goldbach (n+4)) :
 ∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (n+4+2) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 forward g g i
@@ -32,11 +34,61 @@ refine (?_ ∘ g) ?_
     apply Nat.Prime.two_le at hy
     omega
 
+theorem jiting (n : ℕ) :
+(∀ i < n, goldbach (2*i+4)) ->
+∃ j, nth_cfg j = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (2*n+4) Γ.one), Turing.ListBlank.mk []⟩⟩
+ := by
+induction n with
+| zero =>
+have h : nth_cfg 0 = init [] := by simp!
+simp [init, Turing.Tape.mk₁, Turing.Tape.mk₂, Turing.Tape.mk'] at h
+forward h h 0
+forward h h 1
+forward h h 2
+forward h h 3
+forward h h 4
+forward h h 5
+intros _
+use 6
+simp [h]
+tauto
+| succ n =>
+rename_i induction_step
+intros h
+refine (?_ ∘ induction_step) ?_
+. intros g
+  obtain ⟨j, g⟩ := g
+  specialize h n (by omega)
+  apply lemma_25 at g
+  specialize g h
+  obtain ⟨k, g⟩ := g
+  use (j+k)
+  simp [g]
+  ring_nf
+. intros i hi
+  apply h i (by omega)
+
 theorem never_halt (never_none : ∀ i, nth_cfg i ≠ none) (n : ℕ):
-∃ (x y: ℕ), x + y = 2 * n + 4 /\ Nat.Prime x /\ Nat.Prime y
+goldbach (2*n + 4)
 := by
-induction n using Nat.strongRecOn
-. sorry
+induction' n using Nat.strongRecOn with n IH
+apply jiting at IH
+obtain ⟨j, g⟩ := IH
+by_contra! h
+forward g g j
+repeat rw [← List.replicate_succ] at g
+apply (leap_26_halt _ _ 0) at g
+any_goals omega
+refine (?_ ∘ g) ?_
+. intros h
+  obtain ⟨k, h⟩ := h
+  apply never_none _ h
+. intros x y _
+  apply h
+  use! x, y
+  ring_nf at *
+  tauto
+
 
 theorem halt_lemma :
 (∃ (n x y: ℕ), Even n /\ n > 2 /\ x + y = n /\ Nat.Prime x /\ Nat.Prime y) →