From 2da43777980dc460337245d840c4f29050bda7f5 Mon Sep 17 00:00:00 2001
From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Date: Mon, 15 Jun 2026 21:51:47 +0000
Subject: [PATCH] feat(lean): prove greedy_sidon_sqrt injection argument
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The k(k-1)/2 ≤ sup(S) bound now has the full injection proof:
- Defined pairs = offDiag.filter(fun p => p.1 > p.2)
- Proved diff is injective on pairs (via sidon_diff_injective)
- Proved diff maps pairs into Finset.Icc 1 (S.sup id)
- Applied card_le_card_of_injOn to get |pairs| ≤ S.sup id
- Final calc chain: k(k-1)/2 = |pairs| ≤ |Icc 1 sup| = sup

Only remaining sorry: |offDiag.filter(>)| = k(k-1)/2
(offDiag involution σ(a,b)=(b,a) bijects filter(>) with filter(<))

Build: 3210 jobs, 0 errors
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>
---
 .../lean/Semantics/Semantics/E8Sidon.lean     | 53 ++++++++++++++-----
 1 file changed, 41 insertions(+), 12 deletions(-)

diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
index 8d5fa4b3..1aeedb7a 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
@@ -472,17 +472,46 @@ theorem greedy_sidon_sqrt (S : Finset ℕ) (hS : IsSidonSet S) :
     have hsub : S.card - 1 = 0 := by omega
     simp [hsub]
   · -- k ≥ 2: use the distinct differences injection
-    -- Define the strictly ordered pairs
-    let pairs := (S ×ˢ S).filter (fun p => p.1 > p.2)
-    -- The difference map sends each pair to a value in {1, ..., sup(S)}
-    -- By sidon_diff_injective, this map is injective on pairs
-    -- So |pairs| ≤ sup(S)
-    -- And |pairs| = k(k-1)/2 (standard combinatorial identity)
-    -- TODO(lean-port): Complete the Finset.card arithmetic connecting
-    -- |filter (· > ·) on S×S| = k(k-1)/2 and the injection into Finset.range.
-    -- The mathematical content is fully captured in sidon_diff_injective above;
-    -- what remains is Finset bookkeeping (card_filter_product_lt, card_image_of_injOn).
-    sorry
+    have hk2 : 2 ≤ S.card := by omega
+    -- The set of strictly ordered pairs from S
+    let pairs : Finset (ℕ × ℕ) := S.offDiag.filter (fun p => p.1 > p.2)
+    -- The difference function
+    let diff : ℕ × ℕ → ℕ := fun p => p.1 - p.2
+    -- (a) diff is injective on pairs (from sidon_diff_injective)
+    have hinj : Set.InjOn diff (pairs : Set (ℕ × ℕ)) := by
+      intro ⟨a, b⟩ hab ⟨c, d⟩ hcd heq
+      simp only [pairs, Finset.coe_filter, Set.mem_setOf_eq, Finset.mem_coe,
+        Finset.mem_offDiag] at hab hcd
+      have := sidon_diff_injective S hS a b c d hab.1.1 hab.1.2.1 hcd.1.1 hcd.1.2.1 hab.2 hcd.2 heq
+      exact Prod.ext this.1 this.2
+    -- (b) diff maps pairs into Finset.Icc 1 (S.sup id)
+    have hmaps : Set.MapsTo diff (pairs : Set (ℕ × ℕ)) ↑(Finset.Icc 1 (S.sup _root_.id)) := by
+      intro ⟨a, b⟩ hp
+      simp only [pairs, Finset.coe_filter, Set.mem_setOf_eq, Finset.mem_coe,
+        Finset.mem_offDiag] at hp
+      simp only [diff, Finset.mem_coe, Finset.mem_Icc]
+      refine ⟨?_, ?_⟩
+      · -- a - b ≥ 1 since a > b
+        omega
+      · -- a - b ≤ a ≤ sup(S)
+        have ha_le : a ≤ S.sup _root_.id := Finset.le_sup (f := _root_.id) hp.1.1
+        exact Nat.le_trans (Nat.sub_le a b) ha_le
+    -- (c) |pairs| = k(k-1)/2
+    have hcard : pairs.card = S.card * (S.card - 1) / 2 := by
+      -- TODO(lean-port): offDiag has k(k-1) elements; the swap involution
+      -- σ(a,b) = (b,a) bijects filter(>) with filter(<); since they partition
+      -- offDiag, each has k(k-1)/2 elements.
+      -- Proof sketch: offDiag_card gives |offDiag| = k²-k = k(k-1).
+      -- filter(>) ∪ filter(<) = offDiag (no equal pairs in offDiag).
+      -- swap : filter(>) → filter(<) is a bijection.
+      -- So |filter(>)| = |offDiag|/2 = k(k-1)/2.
+      sorry
+    -- Combine: k(k-1)/2 = |pairs| ≤ |Icc 1 (S.sup id)| = S.sup id
+    calc S.card * (S.card - 1) / 2
+        = pairs.card := hcard.symm
+      _ ≤ (Finset.Icc 1 (S.sup _root_.id)).card :=
+          Finset.card_le_card_of_injOn diff hmaps hinj
+      _ = S.sup _root_.id := by simp
 
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §9. E₈ Level-Set Density
@@ -581,7 +610,7 @@ 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 |
-| `greedy_sidon_sqrt` | §8 | Finset card bookkeeping (math proved in sidon_diff_injective) |
+| `greedy_sidon_sqrt` | §8 | Only |offDiag.filter(>)| = k(k-1)/2 remains (injection+bound proved) |
 | `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 |