proof(lean): close e8_levelset_density via σ₃(n) ≤ n⁴ divisor bound

- 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 <noreply@anthropic.com>

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,
+  -- σ₃(n) = ∑_{d|n} d³ ≤ card(div(n)) * n³ ≤ n * n³ = n⁴ ≤ N⁴.
-  -- so E8LevelSet (N^4) N = {1,...,N} and card = N.
+  -- So E8LevelSet (N⁴) N ⊇ [1,N], giving card ≥ N ≥ N/(log 2 N)².
-  -- Then N ≥ N / (Nat.log 2 N)^2 since Nat.log 2 N ≥ 1 for N ≥ 2.
+  have hsub : Finset.Icc 1 N ⊆ E8LevelSet (N ^ 4) N := by
-  sorry
+    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₀]
+-- §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]
+-- §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):
+-- RESTATED + ANALYTIC_OPEN (one sorry remains):
--- §9:  sidon_weight_bound      — LHS corrected: σ₃(a)·σ₃(b) products, not σ₃(a+b) sums
+-- §9:  sidon_weight_bound       — LHS corrected to σ₃(a)·σ₃(b) products over pairs;
--- §10: e8_levelset_density     — T now = N^4 (fixed T refuted by e8_levelset_density_fails)
+--                                  ANALYTIC_OPEN: needs E₈ conv identity summed over Sidon pairs
 
 noncomputable def riemannZeta (s : ℝ) : ℝ :=
   ∑' n : ℕ, (1 : ℝ) / ((n + 1 : ℕ) : ℝ) ^ s