import Mathlib

open Nat

theorem cofactor_ge {m r k q : ℕ} (_hm : 0 < m) (hr : Nat.minFac m = r)
    (hmk : m = r * k) (hq : Nat.Prime q) (hqk : q ∣ k) : r ≤ q := by
  obtain ⟨t, ht⟩ := hqk
  have hqm : q ∣ m := ⟨r * t, by rw [hmk, ht, mul_left_comm]⟩
  rw [← hr]
  exact Nat.minFac_le_of_dvd hq.two_le hqm

theorem prime_of_no_small_divisor {m : ℕ} (hm : 2 ≤ m)
    (h : ∀ q, 2 ≤ q → q * q ≤ m → ¬(q ∣ m)) : Nat.Prime m := by
  set r := Nat.minFac m with hr
  have hrp : Nat.Prime r := Nat.minFac_prime (by omega : m ≠ 1)
  have hr2 : 2 ≤ r := hrp.two_le
  have hdvd : r ∣ m := Nat.minFac_dvd m
  obtain ⟨k, hmk⟩ := hdvd
  by_cases hk : k = 1
  · subst hk
    rw [hmk, Nat.mul_one]
    exact hrp
  · have hkpos : 0 < k := by
      rcases Nat.eq_zero_or_pos k with h | h
      · subst h
        rw [Nat.mul_zero] at hmk
        omega
      · exact h
    have hk2 : 2 ≤ k := by omega
    have hpk : Nat.Prime (Nat.minFac k) := Nat.minFac_prime (by omega : k ≠ 1)
    have hge : r ≤ Nat.minFac k :=
      cofactor_ge (by omega) hr.symm hmk hpk (Nat.minFac_dvd k)
    have hle : Nat.minFac k ≤ k := Nat.le_of_dvd hkpos (Nat.minFac_dvd k)
    have hk3 : r ≤ k := hge.trans hle
    have hsqm : r * r ≤ m := by
      rw [hmk]
      exact Nat.mul_le_mul (le_refl r) hk3
    exact (h r hr2 hsqm ⟨k, hmk⟩).elim

theorem candidate_implies_goldbach (n : ℕ) (hn : 6 ≤ n) (_heven : Even n)
    (p : ℕ) (hp3 : 3 ≤ p) (hp2 : p ≤ n / 2)
    (hcond : ∀ q, 2 ≤ q → q ≤ Nat.sqrt n → ¬(q ∣ p) ∧ ¬(p % q = n % q)) :
    ∃ a b, Nat.Prime a ∧ Nat.Prime b ∧ a + b = n := by
  have hpge2 : 2 ≤ p := by omega
  have hpn : p ≤ n := by omega
  have hpp : Nat.Prime p := by
    refine prime_of_no_small_divisor hpge2 ?_
    intro q hq2 hqq
    have hb1 : q ≤ Nat.sqrt p := Nat.le_sqrt.mpr hqq
    have hb2 : Nat.sqrt p ≤ Nat.sqrt n := Nat.sqrt_le_sqrt hpn
    exact (hcond q hq2 (hb1.trans hb2)).1
  have hbn : 2 ≤ n - p := by omega
  have hnp : Nat.Prime (n - p) := by
    refine prime_of_no_small_divisor hbn ?_
    intro q hq2 hqq hd
    have hr1 : (n - p) % q = 0 := Nat.mod_eq_zero_of_dvd hd
    have hmod : p % q = n % q := by
      have hsplit : n % q = ((n - p) + p) % q := by
        rw [show (n - p) + p = n from by omega]
      rw [hsplit, Nat.add_mod, hr1, Nat.zero_add, Nat.mod_mod]
    have hb1 : q ≤ Nat.sqrt (n - p) := Nat.le_sqrt.mpr hqq
    have hb2 : Nat.sqrt (n - p) ≤ Nat.sqrt n := Nat.sqrt_le_sqrt (by omega)
    exact absurd hmod (hcond q hq2 (hb1.trans hb2)).2
  exact ⟨p, n - p, hpp, hnp, by omega⟩

/- Tests d'anti-vacuité : l'intervalle des modules est non vide,
   et les conditions du candidat sont satisfaites pour au moins
   un témoin concret (sinon l'énoncé serait vrai par vacuité). -/

/-- ANTI-VACUITY TEST n = 10 (témoin p = 5). -/
theorem anti_vacuity_n10 :
    ∃ p, 3 ≤ p ∧ p ≤ 10 / 2 ∧
    ∀ q, 2 ≤ q → q ≤ Nat.sqrt 10 → ¬(q ∣ p) ∧ ¬(p % q = 10 % q) := by
  refine ⟨5, by norm_num, by norm_num, ?_⟩
  intro q h2 hq
  have hs : Nat.sqrt 10 = 3 := by norm_num
  rw [hs] at hq
  have hrange : q = 2 ∨ q = 3 := by omega
  rcases hrange with rfl | rfl <;> norm_num

/-- ANTI-VACUITY TEST n = 30 (témoin p = 7). -/
theorem anti_vacuity_n30 :
    ∃ p, 3 ≤ p ∧ p ≤ 30 / 2 ∧
    ∀ q, 2 ≤ q → q ≤ Nat.sqrt 30 → ¬(q ∣ p) ∧ ¬(p % q = 30 % q) := by
  refine ⟨7, by norm_num, by norm_num, ?_⟩
  intro q h2 hq
  have hs : Nat.sqrt 30 ≤ 5 := by norm_num
  have h5 : q ≤ 5 := by omega
  have hq2 : q = 2 ∨ q = 3 ∨ q = 4 ∨ q = 5 := by omega
  rcases hq2 with rfl | rfl | rfl | rfl <;>
    exact ⟨by decide, by decide⟩

/-- VACUITY GUARD : the module interval is NONEMPTY for n ≥ 6. -/
theorem module_interval_nonempty (n : ℕ) (hn : 6 ≤ n) :
    ∃ q, 2 ≤ q ∧ q ≤ Nat.sqrt n := by
  refine ⟨2, by norm_num, ?_⟩
  have h1 : 2 ≤ Nat.sqrt 6 := by norm_num
  have h2 : Nat.sqrt 6 ≤ Nat.sqrt n := Nat.sqrt_le_sqrt (by omega)
  exact h1.trans h2

#print axioms candidate_implies_goldbach