From 248cf747bfb210a489ea219af7008100928fdb57 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 16 Jun 2026 15:04:04 -0500 Subject: [PATCH] =?UTF-8?q?proof(lean):=20close=20e8=5Flevelset=5Fdensity?= =?UTF-8?q?=20via=20=CF=83=E2=82=83(n)=20=E2=89=A4=20n=E2=81=B4=20divisor?= =?UTF-8?q?=20bound?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - e8_levelset_density (T=N⁴): proven by showing E8LevelSet(N⁴,N) ⊇ [1,N]. Key chain: σ₃(n) = ∑_{d|n} d³ ≤ card(div(n))·n³ ≤ n·n³ = n⁴ ≤ N⁴. card(div(n)) ≤ n from div(n) ⊆ Icc 1 n; then N/(log 2 N)² ≤ N ≤ card. - sidon_weight_bound: one remaining sorry (ANALYTIC_OPEN — E₈ convolution identity summed over Sidon pairs; corrected LHS uses σ₃(a)·σ₃(b) products). - §14 summary updated. Co-Authored-By: Claude Sonnet 4.6 --- .../lean/Semantics/Semantics/E8Sidon.lean | 43 +++++++++++++++---- 1 file changed, 34 insertions(+), 9 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index 594852ff..ec1c5f70 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean @@ -978,10 +978,34 @@ is ANALYTIC_OPEN: requires Dickman function ρ(u) with u = log N / (ε/3 · log -/ theorem e8_levelset_density (N : ℕ) (hN : 100 ≤ N) : (E8LevelSet (N ^ 4) N).card ≥ N / (Nat.log 2 N) ^ 2 := by - -- ANALYTIC_OPEN (but easier than original): σ₃(n) ≤ n^4 ≤ N^4 for n ≤ N, - -- so E8LevelSet (N^4) N = {1,...,N} and card = N. - -- Then N ≥ N / (Nat.log 2 N)^2 since Nat.log 2 N ≥ 1 for N ≥ 2. - sorry + -- σ₃(n) = ∑_{d|n} d³ ≤ card(div(n)) * n³ ≤ n * n³ = n⁴ ≤ N⁴. + -- So E8LevelSet (N⁴) N ⊇ [1,N], giving card ≥ N ≥ N/(log 2 N)². + have hsub : Finset.Icc 1 N ⊆ E8LevelSet (N ^ 4) N := by + intro n hn + rw [Finset.mem_Icc] at hn + simp only [E8LevelSet, Finset.mem_filter, Finset.mem_range] + refine ⟨by omega, hn.1, ?_⟩ + apply le_trans _ (Nat.pow_le_pow_left hn.2 4) + unfold sigma3 sigmaK + have hdivs_sub : n.divisors ⊆ Finset.Icc 1 n := by + intro d hd + rw [Nat.mem_divisors] at hd + rw [Finset.mem_Icc] + have hd_ne : d ≠ 0 := fun h => hd.2 (Nat.zero_dvd.mp (h ▸ hd.1)) + exact ⟨by omega, Nat.le_of_dvd hn.1 hd.1⟩ + have hcard_div : n.divisors.card ≤ n := by + calc n.divisors.card ≤ (Finset.Icc 1 n).card := Finset.card_le_card hdivs_sub + _ = n := by rw [Nat.card_Icc]; omega + calc ∑ d ∈ n.divisors, d ^ 3 + ≤ ∑ _ ∈ n.divisors, n ^ 3 := + Finset.sum_le_sum fun d hd => + Nat.pow_le_pow_left (Nat.le_of_dvd hn.1 (Nat.mem_divisors.mp hd).1) 3 + _ = n.divisors.card * n ^ 3 := by simp [Finset.sum_const, smul_eq_mul] + _ ≤ n * n ^ 3 := Nat.mul_le_mul_right _ hcard_div + _ = n ^ 4 := by ring + have hcard : N ≤ (E8LevelSet (N ^ 4) N).card := + le_trans (by rw [Nat.card_Icc]; omega) (Finset.card_le_card hsub) + exact le_trans (Nat.div_le_self N _) hcard /-- Weaker version: the level set is nonempty for any T ≥ 1 and N ≥ 1. -/ theorem e8_levelset_nonempty (T N : ℕ) (hT : 1 ≤ T) (hN : 1 ≤ N) : @@ -1125,12 +1149,13 @@ theorem erdos30_e8_conditional -- §8: (structure proven, greedy algorithm outlined) -- §9: convWeight_eq -- §10: e8_levelset_nonempty, e8_levelset_mono --- §12: e8_singer_improvement [proven 2026-06-16 via Singer set + pow_le_one₀] --- §13: erdos30_e8_conditional [proven 2026-06-16 via interval_sidon_exists + Nat.sqrt bridge] +-- §12: e8_singer_improvement [proven 2026-06-16 via Singer set + pow_le_one₀] +-- §13: erdos30_e8_conditional [proven 2026-06-16 via interval_sidon_exists + Nat.sqrt bridge] +-- §10: e8_levelset_density [proven 2026-06-16 via σ₃(n)≤n⁴ + divisor count bound] -- --- RESTATED (invalid as originally stated, sorry retained, ANALYTIC_OPEN): --- §9: sidon_weight_bound — LHS corrected: σ₃(a)·σ₃(b) products, not σ₃(a+b) sums --- §10: e8_levelset_density — T now = N^4 (fixed T refuted by e8_levelset_density_fails) +-- RESTATED + ANALYTIC_OPEN (one sorry remains): +-- §9: sidon_weight_bound — LHS corrected to σ₃(a)·σ₃(b) products over pairs; +-- ANALYTIC_OPEN: needs E₈ conv identity summed over Sidon pairs noncomputable def riemannZeta (s : ℝ) : ℝ := ∑' n : ℕ, (1 : ℝ) / ((n + 1 : ℕ) : ℝ) ^ s