proof(E8Sidon): prove e8_levelset_density via Finset.sup'

Close sorry for e8_levelset_density by:
- Adding 0 < n precondition (original statement was false at n=0)
- Using Finset.sup' over Icc 1 N to get finite C
- Showing r8 n ≤ C * 1 ≤ C * n^3

Also improves sidon_energy_bound proof sketch with concrete approach.
Sorry count: 10 tokens across 9 theorems (down from 11/10).

Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>

0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean

@@ -241,11 +241,12 @@ def additiveEnergy (S : Finset ℕ) : ℕ :=
 /-- Sidon sets have additive energy exactly 2|S|² - |S|. -/
 theorem sidon_energy_bound (S : Finset ℕ) (hS : IsSidonSet S) :
     additiveEnergy S ≤ 2 * S.card ^ 2 := by
-  -- TODO(lean-port): prove via IsSidonSet → each sum-fiber has ≤ 2 ordered
-  -- representations (a,b) and (b,a), giving E(S) = 2·|S+S|_{distinct} ≤ 2|S|².
-  -- Proof sketch: count quadruples; for Sidon, {a,b}={c,d} ⟹ (a,b) is a
-  -- permutation of (c,d); each unordered pair gives exactly 2 ordered pairs
-  -- (or 1 if a=b). Total ≤ 2|S|².
+  -- TODO(lean-port): By Sidon, every (a,b,c,d) ∈ S⁴ with a+b=c+d has {a,b}={c,d}.
+  -- So (c,d) = (a,b) or (c,d) = (b,a). The filtered set ⊆ same_set ∪ swap_set,
+  -- each of which injects into S×S via Prod.fst (uniquely determined by first pair).
+  -- Proof approach: from {a,b}={c,d} extract c∈{a,b} via hS_eq.symm ▸ mem_insert,
+  -- then case split on c=a (same) or c=b (swap). Each half has card ≤ k².
+  -- Total ≤ 2k². Blocked on Finset pair-membership simp and product projection API.
   sorry
 
 -- ═══════════════════════════════════════════════════════════════════════════════
@@ -556,13 +557,21 @@ theorem greedy_sidon_sqrt (S : Finset ℕ) (hS : IsSidonSet S) :
     that form a Sidon-like structure. Uses the asymptotic r₈(n) ~ C·n³
     from σ₃(n) growth. -/
 theorem e8_levelset_density (N : ℕ) (hN : 1 ≤ N) :
-    ∃ C : ℕ, ∀ n, n ≤ N → r8 n ≤ C * n ^ 3 := by
-  -- TODO(lean-port): requires Dickman function / smooth number theory bounds
-  -- on σ₃(n). The bound σ₃(n) ≤ C·n³ is elementary (each divisor d ≤ n,
-  -- so d³ ≤ n³, and there are at most n divisors).
-  -- Then r₈(n) = 240·σ₃(n) ≤ 240·n·n³ = 240·n⁴ (crude).
-  -- Better: σ₃(n) ≤ ζ(3)·n³ + O(n²) by Ramanujan's formula.
-  sorry
+    ∃ C : ℕ, ∀ n, 0 < n → n ≤ N → r8 n ≤ C * n ^ 3 := by
+  -- We use the crude bound: σ₇(n) ≤ n * n⁷ = n⁸ (each of ≤n divisors is ≤n⁷).
+  -- Then r8 n = 480 * σ₇(n) ≤ 480 * n⁸ = 480 * n⁵ * n³ ≤ 480 * N⁵ * n³.
+  -- Take C = 480 * N ^ 5 + 1 (the +1 handles the constant term).
+  -- Simpler: since N is finite, take C = sup of {r8(n) | 1 ≤ n ≤ N} + 1.
+  -- Even simpler: the Finset.sup over Icc 1 N of r8 gives a finite max.
+  use (Finset.Icc 1 N).sup' ⟨N, Finset.mem_Icc.mpr ⟨hN, le_refl N⟩⟩ r8
+  intro n hn hnN
+  have hmem : n ∈ Finset.Icc 1 N := Finset.mem_Icc.mpr ⟨hn, hnN⟩
+  have hle : r8 n ≤ (Finset.Icc 1 N).sup' ⟨N, Finset.mem_Icc.mpr ⟨hN, le_refl N⟩⟩ r8 :=
+    Finset.le_sup' r8 hmem
+  calc r8 n ≤ _ := hle
+    _ = _ * 1 := (Nat.mul_one _).symm
+    _ ≤ _ * n ^ 3 := Nat.mul_le_mul_left _ (Nat.one_le_pow 3 n hn)
+    _ = _ := rfl
 
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §10. Conditional Results (open problems)
@@ -665,8 +674,9 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) :
 | `exists_collision_witness` | §8 | ¬Sidon → ∃ collision witness extractable |
 | `greedy_sidon_sqrt` | §8 | Full proof: offDiag involution + injection into Icc 1 sup |
 | `fiber_partition` | §11 | Full proof: swap involution splits fiber into even halves |
+| `e8_levelset_density` | §9 | Full proof: Finset.sup' gives finite C bound |
 
-### Sorry inventory (11 sorry tokens across 10 theorems, all with TODO(lean-port))
+### Sorry inventory (10 sorry tokens across 9 theorems, all with TODO(lean-port))
 
 | Item | Section | Blocked on |
 |------|---------|------------|
@@ -677,7 +687,6 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) :
 | `sidon_iff_zero_collision` | §8 | Finset energy counting (2 sub-sorries) |
 | `collision_excess_decrease` | §8 | Energy decrease bound (Finset filter counting) |
 | `greedy_sidon_extraction` | §8 | Well-founded induction + √ cardinality bound |
-| `e8_levelset_density` | §9 | Elementary σ₃ bound |
 | `e8_singer_improvement` | §10 | Singer difference set construction |
 | `erdos30_e8_conditional` | §10 | Lindström / Erdős–Turán argument |
 -/