allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-13 01:20:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(lean): close sidon_iff_zero_collision (both dirs) and erdos30_e8_conditional

Browse source 
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 <bigdataiscoming+9i37y6j2@protonmail.com>
This commit is contained in:
Devin AI 2026-06-15 23:10:53 +00:00
parent 10feb8d717
commit 5cacb86ddb
3 changed files with 260 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
.cursorrules
View file

@ -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`

9
0-Core-Formalism/lean/Semantics/AGENTS.md
View file

@ -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

274
0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean
View file

@ -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