leap_26

GoldbachTm/Tm31/PBP.lean

@@ -158,22 +158,48 @@ refine (?_ ∘ (lemma_23_to_27 (2+i+j) l1 [] (Γ.zero :: Γ.one :: (List.replica
 
 
 theorem leap_26 (l1 : ℕ) : ∀ (i r1: ℕ),
-l1 + r1 ≥ 2 /\
+l1 + r1 ≥ 2 →
 nth_cfg i = some ⟨⟨26, 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 + 1 /\ Nat.Prime x /\ Nat.Prime y /\ r1 ≤ x /\ x ≤ y) →
+(∃ x y, x + y = l1 + r1 + 2 /\ Nat.Prime x /\ Nat.Prime y /\ (r1+1) ≤ x /\ x ≤ y) →
 ∃ j, nth_cfg (i+j) = some ⟨⟨25, by omega⟩, ⟨Γ.zero, Turing.ListBlank.mk (List.replicate (l1+r1+4) Γ.one), Turing.ListBlank.mk []⟩⟩
 := by
 induction l1 with
 | zero => omega
 | succ l1 =>
   rename_i induction_step
-  intros i r1 h _
-  obtain ⟨h, g⟩ := h
+  intros i r1 h g hpp
   by_cases hp : ¬ Nat.Prime (l1+2) \/ ¬ Nat.Prime (r1+1)
   . -- induction step
     apply lemma_26 at g
     any_goals tauto
-    all_goals sorry
+    obtain ⟨j, g⟩ := g
+    forward g g (i+j)
+    forward g g (1+i+j)
+    repeat rw [← List.replicate_succ] at g
+    apply induction_step at g
+    refine (?_ ∘ g) ?_
+    any_goals omega
+    . intros g
+      obtain ⟨m, g₂⟩ := g
+      use (2+j+m)
+      ring_nf at *
+      simp [g₂]
+    . obtain ⟨x, y, _, _, _, _⟩ := hpp
+      use! x, y
+      repeat any_goals apply And.intro
+      any_goals omega
+      any_goals assumption
+      by_cases x = r1+1
+      any_goals omega
+      subst x
+      exfalso
+      cases hp with
+      | inl hp => apply hp
+                  have : y = l1+2 := by omega
+                  subst y
+                  assumption
+      | inr hp => apply hp
+                  assumption
   . -- both prime
     apply both_prime at g
     all_goals tauto