feat(lean): fully prove greedy_sidon_sqrt and fiber_partition

greedy_sidon_sqrt: Eliminated last sorry. Full proof uses:
  - offDiag involution (Prod.swap bijects filter(>) with filter(<))
  - card_nbij' for the cardinality bijection
  - mul_tsub for k²-k = k(k-1) factoring
  - card_le_card_of_injOn for the injection into Finset.Icc 1 sup

fiber_partition: New full proof that fiber has even cardinality.
  Same involution technique: split into gt/lt halves via swap bijection.

Sorry count reduced from 12 to 11 (10 theorems).

Build: 3210 jobs, 0 errors
Co-Authored-By: Allaun Silverfox <bigdataiscoming+9i37y6j2@protonmail.com>

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

@@ -498,14 +498,49 @@ theorem greedy_sidon_sqrt (S : Finset ℕ) (hS : IsSidonSet S) :
         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
+      -- offDiag splits into filter(>) and filter(<), with swap as bijection
+      let lt_pairs : Finset (ℕ × ℕ) := S.offDiag.filter (fun p => p.1 < p.2)
+      -- They partition offDiag
+      have hunion : pairs ∪ lt_pairs = S.offDiag := by
+        ext ⟨a, b⟩
+        simp only [pairs, lt_pairs, Finset.mem_union, Finset.mem_filter,
+          Finset.mem_offDiag]
+        constructor
+        · rintro (⟨h, _⟩ | ⟨h, _⟩) <;> exact h
+        · intro ⟨ha, hb, hne⟩
+          rcases Nat.lt_or_gt_of_ne hne with hlt | hgt
+          · right; exact ⟨⟨ha, hb, hne⟩, hlt⟩
+          · left; exact ⟨⟨ha, hb, hne⟩, hgt⟩
+      have hdisj : Disjoint pairs lt_pairs := by
+        rw [Finset.disjoint_filter]
+        intro ⟨a, b⟩ _ hgt hlt; omega
+      -- Swap bijects pairs ↔ lt_pairs
+      have hbij : pairs.card = lt_pairs.card :=
+        Finset.card_nbij' Prod.swap Prod.swap
+          (by -- MapsTo swap pairs lt_pairs
+            intro ⟨a, b⟩ hp
+            simp only [pairs, lt_pairs, Finset.mem_coe, Finset.mem_filter,
+              Finset.mem_offDiag, Prod.swap] at hp ⊢
+            exact ⟨⟨hp.1.2.1, hp.1.1, Ne.symm hp.1.2.2⟩, hp.2⟩)
+          (by -- MapsTo swap lt_pairs pairs
+            intro ⟨a, b⟩ hp
+            simp only [lt_pairs, pairs, Finset.mem_coe, Finset.mem_filter,
+              Finset.mem_offDiag, Prod.swap] at hp ⊢
+            exact ⟨⟨hp.1.2.1, hp.1.1, Ne.symm hp.1.2.2⟩, hp.2⟩)
+          (by intro ⟨_, _⟩ _; rfl)
+          (by intro ⟨_, _⟩ _; rfl)
+      -- |pairs| + |lt_pairs| = |offDiag| = k²-k
+      have hsum : pairs.card + lt_pairs.card = S.offDiag.card := by
+        rw [← Finset.card_union_of_disjoint hdisj, hunion]
+      have hoff : S.offDiag.card = S.card * S.card - S.card := S.offDiag_card
+      -- 2 * |pairs| = k(k-1), so |pairs| = k(k-1)/2
+      have hfact : S.card * S.card - S.card = S.card * (S.card - 1) := by
+        have h := mul_tsub S.card S.card 1
+        rw [Nat.mul_one] at h
+        exact h.symm
+      have h_two : 2 * pairs.card = S.offDiag.card := by omega
+      rw [hoff, hfact] at h_two
+      omega
     -- 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
@@ -570,16 +605,46 @@ theorem erdos30_e8_conditional (N : ℕ) (hN : 1 ≤ N)
     has even cardinality (pairing (a,b) with (b,a)), except when a = b. -/
 theorem fiber_partition (S : Finset ℕ) (s : ℕ) :
     Even (((S ×ˢ S).filter (fun (a, b) => a + b = s ∧ a ≠ b)).card) := by
-  -- The involution (a,b) ↦ (b,a) pairs off all elements with a ≠ b
-  have hinv : ∀ p ∈ (S ×ˢ S).filter (fun (a, b) => a + b = s ∧ a ≠ b),
-    (p.2, p.1) ∈ (S ×ˢ S).filter (fun (a, b) => a + b = s ∧ a ≠ b) := by
-    intro ⟨a, b⟩ hp
-    simp only [Finset.mem_filter, Finset.mem_product] at hp ⊢
-    exact ⟨⟨hp.1.2, hp.1.1⟩, by omega, hp.2.2.symm⟩
-  -- TODO(lean-port): Complete using Finset.card_even_of_involution
-  -- with the involution σ(a,b) = (b,a), which is fixed-point-free on
-  -- the fiber where a ≠ b.
-  sorry
+  -- Split into gt-half and lt-half, swap bijects them
+  let fiber := (S ×ˢ S).filter (fun (a, b) => a + b = s ∧ a ≠ b)
+  let gt_half := fiber.filter (fun p => p.1 > p.2)
+  let lt_half := fiber.filter (fun p => p.1 < p.2)
+  -- They partition fiber (since a ≠ b on fiber means a > b or a < b)
+  have hunion : gt_half ∪ lt_half = fiber := by
+    ext ⟨a, b⟩
+    simp only [gt_half, lt_half, fiber, Finset.mem_union, Finset.mem_filter,
+      Finset.mem_product]
+    constructor
+    · rintro (⟨h, _⟩ | ⟨h, _⟩) <;> exact h
+    · intro ⟨⟨ha, hb⟩, hsum, hne⟩
+      rcases Nat.lt_or_gt_of_ne hne with hlt | hgt
+      · right; exact ⟨⟨⟨ha, hb⟩, hsum, hne⟩, hlt⟩
+      · left; exact ⟨⟨⟨ha, hb⟩, hsum, hne⟩, hgt⟩
+  have hdisj : Disjoint gt_half lt_half := by
+    rw [Finset.disjoint_filter]; intro ⟨a, b⟩ _ hgt hlt; omega
+  -- Swap bijects gt_half ↔ lt_half
+  have hbij : gt_half.card = lt_half.card :=
+    Finset.card_nbij' Prod.swap Prod.swap
+      (by
+        intro ⟨a, b⟩ hp
+        simp only [gt_half, lt_half, fiber, Finset.mem_coe, Finset.mem_filter,
+          Finset.mem_product, Prod.swap] at hp ⊢
+        obtain ⟨⟨⟨ha, hb⟩, hsum, hne⟩, hgt⟩ := hp
+        exact ⟨⟨⟨hb, ha⟩, by omega, Ne.symm hne⟩, hgt⟩)
+      (by
+        intro ⟨a, b⟩ hp
+        simp only [lt_half, gt_half, fiber, Finset.mem_coe, Finset.mem_filter,
+          Finset.mem_product, Prod.swap] at hp ⊢
+        obtain ⟨⟨⟨ha, hb⟩, hsum, hne⟩, hlt⟩ := hp
+        exact ⟨⟨⟨hb, ha⟩, by omega, Ne.symm hne⟩, hlt⟩)
+      (by intro ⟨_, _⟩ _; rfl)
+      (by intro ⟨_, _⟩ _; rfl)
+  -- card = 2 * |gt_half|
+  have hcard : fiber.card = 2 * gt_half.card := by
+    have hsum := Finset.card_union_of_disjoint hdisj
+    rw [hunion] at hsum; omega
+  show Even fiber.card
+  exact ⟨gt_half.card, by omega⟩
 
 -- ═══════════════════════════════════════════════════════════════════════════════
 -- §12. Summary of Sorry/Axiom Inventory
@@ -598,8 +663,10 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) :
 |------|---------|-------|
 | `sidon_diff_injective` | §8 | Core lemma: Sidon → distinct positive differences |
 | `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 |
 
-### Sorry inventory (12 total, all with TODO(lean-port))
+### Sorry inventory (11 sorry tokens across 10 theorems, all with TODO(lean-port))
 
 | Item | Section | Blocked on |
 |------|---------|------------|
@@ -610,11 +677,9 @@ 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 | 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 |
-| `fiber_partition` | §11 | Finset involution lemma |
 -/
 
 end Semantics.E8Sidon