From 5cacb86ddb9a9017086329b55eb39d5ac1ea6aa5 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Mon, 15 Jun 2026 23:10:53 +0000 Subject: [PATCH] feat(lean): close sidon_iff_zero_collision (both dirs) and erdos30_e8_conditional MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Close 3 sorry tokens (forward, backward, erdos30): - sidon_iff_zero_collision forward: double-inclusion proves filter = same∪swap, inclusion-exclusion gives card = (2k-1)k exactly. - sidon_iff_zero_collision backward: cardinality squeeze shows filter = same∪swap when excess=0, then classify each element via same/swap membership. - erdos30_e8_conditional: difference injection into Icc 1 N + trichotomy partition gives k(k-1) ≤ 2N, contraposition via nlinarith closes the bound. E8Sidon sorry count: 9 → 6 (across 6 theorems). All remaining sorries documented with TODO(lean-port). Build: 3572 jobs, 0 errors (lake build) Co-Authored-By: Allaun Silverfox --- .cursorrules | 8 +- 0-Core-Formalism/lean/Semantics/AGENTS.md | 9 +- .../lean/Semantics/Semantics/E8Sidon.lean | 274 ++++++++++++++++-- 3 files changed, 260 insertions(+), 31 deletions(-) diff --git a/.cursorrules b/.cursorrules index d1e7c8b6..e8b37060 100644 --- a/.cursorrules +++ b/.cursorrules @@ -18,12 +18,13 @@ v0.4.74 ## Research Stack — Current Project State (2026-05-28) -**Build:** `lake build` — 3571 jobs, 0 errors +**Build:** `lake build` — 3572 jobs, 0 errors (reverified 2026-06-15) **Python tests:** 68/68 pass -**Sorry inventory:** 8 total (all with `TODO(lean-port)` documentation) +**Sorry inventory:** 14 total (all with `TODO(lean-port)` documentation) - `AdjugateMatrix`: 3 sorries - `FourPrimitiveErdosRenyi`: 4 sorries - `HyperbolicStateSurface`: 1 sorry + - `E8Sidon`: 6 sorries (3 Mathlib-blocked, 3 hard infrastructure) ### Key Architecture Decisions - **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant) @@ -32,7 +33,8 @@ v0.4.74 - **Golden ratio unit separation** formalized in Lean ### New Lean Modules -`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE` +`AdjugateMatrix`, `OptimizedRoute`, `GoldenRatioSeparation`, `BraidBitwiseODE`, +`E8Sidon`, `FixedPointBoundary` ### New Python Modules `qubo_highs.py`, `alphaproof_loop.py`, `scale_space_solver.py` diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index b94adc72..6d3a9d15 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -223,10 +223,15 @@ after narrowly compiling the file under a scratch target. Blocked on Mathlib missing the valence formula or dim M₈(SL₂ℤ) = 1. Proof path: apply valence formula → E₄² − E₈ = 0 → extract coefficients. Computationally verified for n = 2, 3, 4 via `#eval`. - - 11 additional sorries (Sidon energy bound, greedy extraction, collision - theory, level-set density, Singer improvement, fiber partition). All have + - 5 additional sorries (`r8_via_sigma3`, `r8_one`, `collision_excess_decrease`, + `greedy_sidon_extraction`, `e8_singer_improvement`). All have `TODO(lean-port)` with proof sketches. - 1 axiom: `e8_additive_completeness` (open problem in additive combinatorics). + - Fully proved: `sidon_iff_zero_collision` (both directions via double-inclusion + + cardinality squeeze), `erdos30_e8_conditional` (Erdős–Turán bound via + difference injection + trichotomy partition), `sidon_energy_bound`, + `sidon_diff_injective`, `greedy_sidon_sqrt`, `fiber_partition`, + `e8_levelset_density`, `exists_collision_witness`. - Definitions (`sigma3`, `sigma7`, `convolutionLHS`, `IsSidonSet`, `r8`) and Bernoulli evaluations (`bernoulli_four`, `bernoulli_eight`) fully proven. - `goldenContractionEnergyDecrease` is discharged. Remaining follow-up is a diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index f2ecdf7b..6bc71ef5 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean @@ -345,27 +345,167 @@ theorem sidon_iff_zero_collision (S : Finset ℕ) : · -- Forward: IsSidonSet → excess = 0 intro hS unfold totalCollisionExcess - -- For Sidon S, additiveEnergy S = (2 * S.card - 1) * S.card - -- because every solution (a,b,c,d) to a+b=c+d has {a,b}={c,d}, - -- meaning (c,d) is a permutation of (a,b). This gives exactly - -- 2 solutions per off-diagonal pair and 1 per diagonal entry. suffices h : additiveEnergy S = (2 * S.card - 1) * S.card by omega - -- TODO(lean-port): prove additiveEnergy = (2k-1)k for Sidon sets. - -- Requires showing the filter on S⁴ has exactly (2k²-k) elements - -- via the Sidon partition: each unordered pair {a,b} contributes - -- 2 ordered solutions (or 1 if a=b), totaling 2·C(k,2) + k = 2k²-k. - sorry - · -- Backward: excess = 0 → IsSidonSet + unfold additiveEnergy + set filt := ((S ×ˢ S) ×ˢ (S ×ˢ S)).filter + (fun x : (ℕ × ℕ) × (ℕ × ℕ) => x.1.1 + x.1.2 = x.2.1 + x.2.2) + set same := (S ×ˢ S).image (fun p : ℕ × ℕ => (p, p)) + set swap := (S ×ˢ S).image (fun p : ℕ × ℕ => (p, (p.2, p.1))) + -- Filter = same ∪ swap (double inclusion) + have hsub : filt ⊆ same ∪ swap := by + intro ⟨⟨a, b⟩, ⟨c, d⟩⟩ hmem + simp only [filt, Finset.mem_filter, Finset.mem_product] at hmem + obtain ⟨⟨⟨ha, hb⟩, hc, hd⟩, hsum⟩ := hmem + have hab_mem : (a, b) ∈ S ×ˢ S := Finset.mem_product.mpr ⟨ha, hb⟩ + rcases finset_pair_eq_iff (hS a b c d ha hb hc hd hsum) with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ + · exact Finset.mem_union_left _ (Finset.mem_image.mpr ⟨(a, b), hab_mem, rfl⟩) + · exact Finset.mem_union_right _ (Finset.mem_image.mpr ⟨(a, b), hab_mem, rfl⟩) + have hsup : same ∪ swap ⊆ filt := by + intro x hx + rcases Finset.mem_union.mp hx with h | h + · obtain ⟨⟨a, b⟩, hmem, rfl⟩ := Finset.mem_image.mp h + have ⟨ha, hb⟩ := Finset.mem_product.mp hmem + simp [filt, Finset.mem_filter, Finset.mem_product, ha, hb] + · obtain ⟨⟨a, b⟩, hmem, rfl⟩ := Finset.mem_image.mp h + have ⟨ha, hb⟩ := Finset.mem_product.mp hmem + simp [filt, Finset.mem_filter, Finset.mem_product, ha, hb, Nat.add_comm] + have heq : filt = same ∪ swap := Finset.Subset.antisymm hsub hsup + rw [heq] + -- Cardinalities via inclusion-exclusion + have h_same_card : same.card = S.card ^ 2 := by + simp only [same] + rw [Finset.card_image_of_injective _ (fun _ _ h => (Prod.mk.inj h).1), + Finset.card_product]; ring + have h_swap_card : swap.card = S.card ^ 2 := by + simp only [swap] + rw [Finset.card_image_of_injective _ (fun _ _ h => (Prod.mk.inj h).1), + Finset.card_product]; ring + have h_inter_card : (same ∩ swap).card = S.card := by + apply le_antisymm + · have h_sub_diag : same ∩ swap ⊆ S.image (fun a => ((a, a), (a, a))) := by + intro x hx + have ⟨h1, h2⟩ := Finset.mem_inter.mp hx + obtain ⟨⟨u, v⟩, huv, rfl⟩ := Finset.mem_image.mp h1 + obtain ⟨⟨s, t⟩, _, h_eq⟩ := Finset.mem_image.mp h2 + have h_fst : (s, t) = (u, v) := congr_arg Prod.fst h_eq + have h_snd : (t, s) = (u, v) := congr_arg Prod.snd h_eq + have : u = v := by + have ht : t = v := congr_arg Prod.snd h_fst + have ht2 : t = u := congr_arg Prod.fst h_snd + linarith + subst this + exact Finset.mem_image.mpr ⟨u, (Finset.mem_product.mp huv).1, rfl⟩ + calc (same ∩ swap).card ≤ (S.image (fun a => ((a, a), (a, a)))).card := + Finset.card_le_card h_sub_diag + _ ≤ S.card := Finset.card_image_le + · have h_diag_sub : S.image (fun a => ((a, a), (a, a))) ⊆ same ∩ swap := by + intro x hx + obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx + have haa : (a, a) ∈ S ×ˢ S := Finset.mem_product.mpr ⟨ha, ha⟩ + exact Finset.mem_inter.mpr ⟨ + Finset.mem_image.mpr ⟨(a, a), haa, rfl⟩, + Finset.mem_image.mpr ⟨(a, a), haa, rfl⟩⟩ + calc S.card = (S.image (fun a => ((a, a), (a, a)))).card := + (Finset.card_image_of_injective _ + (fun a b h => by simpa using congr_arg (Prod.fst ∘ Prod.fst) h)).symm + _ ≤ (same ∩ swap).card := Finset.card_le_card h_diag_sub + have h_ie := Finset.card_union_add_card_inter same swap + have h_nat : (2 * S.card - 1) * S.card + S.card = 2 * S.card ^ 2 := by + cases S.card with + | zero => simp + | succ n => + have hh : 2 * (n + 1) - 1 = 2 * n + 1 := by omega + rw [hh]; ring + linarith + · -- Backward: excess = 0 → IsSidonSet (cardinality squeeze) intro hexcess unfold totalCollisionExcess at hexcess - -- excess = 0 means additiveEnergy S = (2k-1)k (since energy ≥ baseline always) + unfold additiveEnergy at hexcess + set filt := ((S ×ˢ S) ×ˢ (S ×ˢ S)).filter + (fun x : (ℕ × ℕ) × (ℕ × ℕ) => x.1.1 + x.1.2 = x.2.1 + x.2.2) + set same := (S ×ˢ S).image (fun p : ℕ × ℕ => (p, p)) + set swap := (S ×ˢ S).image (fun p : ℕ × ℕ => (p, (p.2, p.1))) + -- same ∪ swap ⊆ filt (trivial: a+b=a+b and a+b=b+a) + have hsup : same ∪ swap ⊆ filt := by + intro x hx + rcases Finset.mem_union.mp hx with h | h + · obtain ⟨⟨a, b⟩, hmem, rfl⟩ := Finset.mem_image.mp h + have ⟨ha, hb⟩ := Finset.mem_product.mp hmem + simp [filt, Finset.mem_filter, Finset.mem_product, ha, hb] + · obtain ⟨⟨a, b⟩, hmem, rfl⟩ := Finset.mem_image.mp h + have ⟨ha, hb⟩ := Finset.mem_product.mp hmem + simp [filt, Finset.mem_filter, Finset.mem_product, ha, hb, Nat.add_comm] + -- card(same ∪ swap) = (2k-1)*k + have h_same_card : same.card = S.card ^ 2 := by + simp only [same] + rw [Finset.card_image_of_injective _ (fun _ _ h => (Prod.mk.inj h).1), + Finset.card_product]; ring + have h_swap_card : swap.card = S.card ^ 2 := by + simp only [swap] + rw [Finset.card_image_of_injective _ (fun _ _ h => (Prod.mk.inj h).1), + Finset.card_product]; ring + have h_inter_card : (same ∩ swap).card = S.card := by + apply le_antisymm + · have h_sub_diag : same ∩ swap ⊆ S.image (fun a => ((a, a), (a, a))) := by + intro x hx + have ⟨h1, h2⟩ := Finset.mem_inter.mp hx + obtain ⟨⟨u, v⟩, huv, rfl⟩ := Finset.mem_image.mp h1 + obtain ⟨⟨s, t⟩, _, h_eq⟩ := Finset.mem_image.mp h2 + have h_fst : (s, t) = (u, v) := congr_arg Prod.fst h_eq + have h_snd : (t, s) = (u, v) := congr_arg Prod.snd h_eq + have : u = v := by + have ht : t = v := congr_arg Prod.snd h_fst + have ht2 : t = u := congr_arg Prod.fst h_snd + linarith + subst this + exact Finset.mem_image.mpr ⟨u, (Finset.mem_product.mp huv).1, rfl⟩ + calc (same ∩ swap).card ≤ (S.image (fun a => ((a, a), (a, a)))).card := + Finset.card_le_card h_sub_diag + _ ≤ S.card := Finset.card_image_le + · have h_diag_sub : S.image (fun a => ((a, a), (a, a))) ⊆ same ∩ swap := by + intro x hx + obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx + have haa : (a, a) ∈ S ×ˢ S := Finset.mem_product.mpr ⟨ha, ha⟩ + exact Finset.mem_inter.mpr ⟨ + Finset.mem_image.mpr ⟨(a, a), haa, rfl⟩, + Finset.mem_image.mpr ⟨(a, a), haa, rfl⟩⟩ + calc S.card = (S.image (fun a => ((a, a), (a, a)))).card := + (Finset.card_image_of_injective _ + (fun a b h => by simpa using congr_arg (Prod.fst ∘ Prod.fst) h)).symm + _ ≤ (same ∩ swap).card := Finset.card_le_card h_diag_sub + have h_ie := Finset.card_union_add_card_inter same swap + have h_union_card : (same ∪ swap).card = (2 * S.card - 1) * S.card := by + have h_nat : (2 * S.card - 1) * S.card + S.card = 2 * S.card ^ 2 := by + cases S.card with + | zero => simp + | succ n => + have hh : 2 * (n + 1) - 1 = 2 * n + 1 := by omega + rw [hh]; ring + linarith + -- Cardinality squeeze: filt.card ≤ (same ∪ swap).card + have h_filt_le : filt.card ≤ (same ∪ swap).card := by + rw [h_union_card]; omega + -- Therefore filt = same ∪ swap + have heq : filt = same ∪ swap := + (Finset.eq_of_subset_of_card_le hsup h_filt_le).symm + -- Prove IsSidonSet: classify each element intro a b c d ha hb hc hd hsum - -- If {a,b} ≠ {c,d}, we get extra quadruples beyond baseline → contradiction - -- TODO(lean-port): prove by contradiction. If {a,b} ≠ {c,d} with a+b=c+d, - -- then (a,b,c,d), (b,a,c,d), (a,b,d,c), (b,a,d,c) are 4 solutions. - -- Combined with the baseline (2k-1)k solutions from trivial pairs, - -- total energy > (2k-1)k, contradicting excess = 0. - sorry + have hmem_filt : ((a, b), (c, d)) ∈ filt := by + simp [filt, Finset.mem_filter, Finset.mem_product, ha, hb, hc, hd, hsum] + rw [heq] at hmem_filt + rcases Finset.mem_union.mp hmem_filt with h | h + · obtain ⟨⟨u, v⟩, _, huv⟩ := Finset.mem_image.mp h + have h1 : (u, v) = (a, b) := congr_arg Prod.fst huv + have h2 : (u, v) = (c, d) := congr_arg Prod.snd huv + have hac : a = c := by linarith [congr_arg Prod.fst h1, congr_arg Prod.fst h2] + have hbd : b = d := by linarith [congr_arg Prod.snd h1, congr_arg Prod.snd h2] + rw [hac, hbd] + · obtain ⟨⟨u, v⟩, _, huv⟩ := Finset.mem_image.mp h + have h1 : (u, v) = (a, b) := congr_arg Prod.fst huv + have h2 : (v, u) = (c, d) := congr_arg Prod.snd huv + have hcb : c = b := by linarith [congr_arg Prod.fst h2, congr_arg Prod.snd h1] + have hda : d = a := by linarith [congr_arg Prod.snd h2, congr_arg Prod.fst h1] + rw [hcb, hda]; exact Finset.pair_comm a b /-- Extracting a colliding element strictly decreases collision excess. @@ -631,12 +771,94 @@ theorem e8_singer_improvement (q : ℕ) (hq : Nat.Prime q) : theorem erdos30_e8_conditional (N : ℕ) (hN : 1 ≤ N) (S : Finset ℕ) (hS : IsSidonSet S) (hbound : ∀ x ∈ S, x ≤ N) : S.card ≤ 2 * Nat.sqrt N + 1 := by - -- TODO(lean-port): conditional on the open axiom e8_additive_completeness. - -- The bound S.card ≤ √N + √(N^{1/4}) + 1 follows from the Lindström - -- argument: if |S| > √N + O(N^{1/4}), then the sumset S+S has too - -- many collisions in {1,...,2N}, contradicting IsSidonSet. - -- The factor 2 in "2·√N+1" is the unconditional Erdős–Turán bound. - sorry + suffices h_count : S.card * (S.card - 1) ≤ 2 * N by + by_contra h_neg + push_neg at h_neg + have hk : S.card ≥ 2 * Nat.sqrt N + 2 := h_neg + have h1 : S.card * (S.card - 1) ≥ (2 * Nat.sqrt N + 2) * (2 * Nat.sqrt N + 1) := + Nat.mul_le_mul hk (by omega : S.card - 1 ≥ 2 * Nat.sqrt N + 1) + have h3 : N < (Nat.sqrt N + 1) ^ 2 := Nat.lt_succ_sqrt' N + nlinarith [sq_nonneg (Nat.sqrt N)] + -- Step 1: card(pairs with a > b) ≤ N via injection into {1,...,N} + set gt_pairs := (S ×ˢ S).filter (fun p : ℕ × ℕ => p.1 > p.2) with gt_pairs_def + have h_dp_le : gt_pairs.card ≤ N := by + have h_maps : ∀ p ∈ gt_pairs, p.1 - p.2 ∈ (Finset.Icc 1 N : Finset ℕ) := by + intro p hp + have ⟨hp_prod, hp_gt⟩ := Finset.mem_filter.mp hp + exact Finset.mem_Icc.mpr ⟨Nat.sub_pos_of_lt hp_gt, + le_trans (Nat.sub_le p.1 p.2) (hbound p.1 (Finset.mem_product.mp hp_prod).1)⟩ + have h_inj : ∀ p ∈ gt_pairs, ∀ q ∈ gt_pairs, p.1 - p.2 = q.1 - q.2 → p = q := by + intro p hp q hq heq + have ⟨hp_prod, hp_gt⟩ := Finset.mem_filter.mp hp + have ⟨hq_prod, hq_gt⟩ := Finset.mem_filter.mp hq + exact Prod.ext + (sidon_diff_injective S hS p.1 p.2 q.1 q.2 + (Finset.mem_product.mp hp_prod).1 (Finset.mem_product.mp hp_prod).2 + (Finset.mem_product.mp hq_prod).1 (Finset.mem_product.mp hq_prod).2 hp_gt hq_gt heq).1 + (sidon_diff_injective S hS p.1 p.2 q.1 q.2 + (Finset.mem_product.mp hp_prod).1 (Finset.mem_product.mp hp_prod).2 + (Finset.mem_product.mp hq_prod).1 (Finset.mem_product.mp hq_prod).2 hp_gt hq_gt heq).2 + have h_img_sub : gt_pairs.image (fun p : ℕ × ℕ => p.1 - p.2) ⊆ Finset.Icc 1 N := by + intro d hd; obtain ⟨p, hp, rfl⟩ := Finset.mem_image.mp hd; exact h_maps p hp + calc gt_pairs.card + = (gt_pairs.image (fun p : ℕ × ℕ => p.1 - p.2)).card := + (Finset.card_image_of_injOn h_inj).symm + _ ≤ (Finset.Icc 1 N : Finset ℕ).card := Finset.card_le_card h_img_sub + _ = N := by have := @Nat.card_Icc 1 N; omega + -- Step 2: partition gives 2*gt + k = k² + have h_decomp : 2 * gt_pairs.card + S.card = S.card * S.card := by + set lt_pairs := (S ×ˢ S).filter (fun p : ℕ × ℕ => p.1 < p.2) + set eq_pairs := (S ×ˢ S).filter (fun p : ℕ × ℕ => p.1 = p.2) + have h_swap : lt_pairs.card = gt_pairs.card := by + apply Finset.card_nbij (fun p : ℕ × ℕ => (p.2, p.1)) + · intro p hp + have ⟨hp_prod, hp_lt⟩ := Finset.mem_filter.mp hp + exact Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨(Finset.mem_product.mp hp_prod).2, + (Finset.mem_product.mp hp_prod).1⟩, hp_lt⟩ + · intro p _ q _ h; exact Prod.ext (congr_arg Prod.snd h) (congr_arg Prod.fst h) + · intro p hp + have ⟨hp_prod, hp_gt⟩ := Finset.mem_filter.mp hp + refine ⟨(p.2, p.1), Finset.mem_filter.mpr ⟨Finset.mem_product.mpr + ⟨(Finset.mem_product.mp hp_prod).2, (Finset.mem_product.mp hp_prod).1⟩, hp_gt⟩, ?_⟩ + ext <;> rfl + have h_diag : eq_pairs.card = S.card := by + apply Finset.card_nbij (fun p : ℕ × ℕ => p.1) + · intro p hp; exact (Finset.mem_product.mp (Finset.mem_filter.mp hp).1).1 + · intro p hp q hq heq + have hp_eq : p.1 = p.2 := (Finset.mem_filter.mp hp).2 + have hq_eq : q.1 = q.2 := (Finset.mem_filter.mp hq).2 + exact Prod.ext heq (by linarith) + · intro a ha + exact ⟨(a, a), Finset.mem_filter.mpr ⟨Finset.mem_product.mpr ⟨ha, ha⟩, rfl⟩, rfl⟩ + have h_d12 : Disjoint gt_pairs lt_pairs := + Finset.disjoint_filter.mpr (fun p _ h1 h2 => by omega) + have h_d3 : Disjoint (gt_pairs ∪ lt_pairs) eq_pairs := by + rw [Finset.disjoint_union_left] + exact ⟨Finset.disjoint_filter.mpr (fun p _ h1 h2 => by omega), + Finset.disjoint_filter.mpr (fun p _ h1 h2 => by omega)⟩ + have h_cover : S ×ˢ S = gt_pairs ∪ lt_pairs ∪ eq_pairs := by + ext p; constructor + · intro hp + rcases Nat.lt_trichotomy p.1 p.2 with hlt | heq | hgt + · exact Finset.mem_union.mpr (Or.inl (Finset.mem_union.mpr + (Or.inr (Finset.mem_filter.mpr ⟨hp, hlt⟩)))) + · exact Finset.mem_union.mpr (Or.inr (Finset.mem_filter.mpr ⟨hp, heq⟩)) + · exact Finset.mem_union.mpr (Or.inl (Finset.mem_union.mpr + (Or.inl (Finset.mem_filter.mpr ⟨hp, hgt⟩)))) + · intro hp + rcases Finset.mem_union.mp hp with h | h + · rcases Finset.mem_union.mp h with h1 | h1 <;> exact (Finset.mem_filter.mp h1).1 + · exact (Finset.mem_filter.mp h).1 + have h_tri : (S ×ˢ S).card = gt_pairs.card + lt_pairs.card + eq_pairs.card := by + conv_lhs => rw [h_cover] + rw [Finset.card_union_of_disjoint h_d3, Finset.card_union_of_disjoint h_d12] + rw [Finset.card_product] at h_tri; linarith + -- Step 3: Final arithmetic — k*(k-1) ≤ 2*N + have h_nat : S.card * (S.card - 1) + S.card = S.card * S.card := by + cases S.card with + | zero => simp + | succ n => simp [Nat.succ_sub_one]; ring + linarith -- ═══════════════════════════════════════════════════════════════════════════════ -- §11. Fiber Partition Lemma @@ -704,24 +926,24 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) : |------|---------|-------| | `finset_pair_eq_iff` | §5 | RRC classification: {a,b}={c,d} → same∨swap via Set.pair_eq_pair_iff | | `sidon_energy_bound` | §6 | Full proof: dimensional routing to same∪swap, each ≤ k² | +| `sidon_iff_zero_collision` | §8 | Full proof: double-inclusion + inclusion-exclusion cardinality squeeze | | `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 | +| `erdos30_e8_conditional` | §10 | Full proof: difference injection + trichotomy partition + nlinarith | | `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 (9 sorry tokens across 8 theorems, all with TODO(lean-port)) +### Sorry inventory (6 sorry tokens across 6 theorems, all with TODO(lean-port)) | Item | Section | Blocked on | |------|---------|------------| | `E4_sq_eq_E8_coeff` | §4 | Mathlib: valence formula or dim M₈ = 1 | | `r8_via_sigma3` | §7 | Same as E4_sq_eq_E8_coeff (Θ_{E₈} = E₄) | | `r8_one` | §7 | Definition mismatch; needs Θ_{E₈} = E₄ | -| `sidon_iff_zero_collision` | §8 | Exact cardinality of same∩swap (2 sub-sorries) | | `collision_excess_decrease` | §8 | Energy decrease bound (Finset filter counting) | | `greedy_sidon_extraction` | §8 | Well-founded induction + √ cardinality bound | | `e8_singer_improvement` | §10 | Singer difference set construction | -| `erdos30_e8_conditional` | §10 | Lindström / Erdős–Turán argument | -/ end Semantics.E8Sidon