From 86f9c3b537d98805468ace6a7adf00b1ae417abd Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Mon, 15 Jun 2026 22:00:58 +0000 Subject: [PATCH] feat(lean): fully prove greedy_sidon_sqrt and fiber_partition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../lean/Semantics/Semantics/E8Sidon.lean | 107 ++++++++++++++---- 1 file changed, 86 insertions(+), 21 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index 1aeedb7a..39d95980 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/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