diff --git a/.cursorrules b/.cursorrules index e8b37060..fb0aa3c2 100644 --- a/.cursorrules +++ b/.cursorrules @@ -20,11 +20,12 @@ v0.4.74 **Build:** `lake build` — 3572 jobs, 0 errors (reverified 2026-06-15) **Python tests:** 68/68 pass -**Sorry inventory:** 14 total (all with `TODO(lean-port)` documentation) +**Sorry inventory:** 12 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) + - `E8Sidon`: 4 sorries (1 Mathlib-blocked: `E4_sq_eq_E8_qExpansion` = dim M₈=1; + 3 hard infrastructure). `E4_sq_eq_E8_coeff` fully reduced to that one gap. ### Key Architecture Decisions - **Q16_16 fixed-point arithmetic** throughout — no Float in hot paths (AGENTS.md §1.4 compliant) diff --git a/0-Core-Formalism/lean/Semantics/AGENTS.md b/0-Core-Formalism/lean/Semantics/AGENTS.md index 6d3a9d15..e865a022 100644 --- a/0-Core-Formalism/lean/Semantics/AGENTS.md +++ b/0-Core-Formalism/lean/Semantics/AGENTS.md @@ -219,14 +219,22 @@ after narrowly compiling the file under a scratch target. ## Pending Proof Work - `Semantics.E8Sidon` — E₈ lattice Sidon framework (new module). - - `E4_sq_eq_E8_coeff`: coefficient identity from E₄² = E₈. - 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`. - - 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. + 4 sorry tokens across 4 theorems (down from 12), all with `TODO(lean-port)`. + - `E4_sq_eq_E8_qExpansion`: the single irreducible Mathlib gap — `E₄² = E₈` + as q-expansions. Blocked on `dim M₈(SL₂ℤ) = 1` / valence formula, absent in + Mathlib v4.30 (`LevelOne.lean` proves `Module.rank` only for weight ≤ 0 and + carries an explicit "TODO: Add finite-dimensionality"). This is the *only* + residual gap in the whole E₄²=E₈ chain. + - `collision_excess_decrease`, `greedy_sidon_extraction`, + `e8_singer_improvement`: Finset/infrastructure-heavy, with proof sketches. - 1 axiom: `e8_additive_completeness` (open problem in additive combinatorics). + - `E4_sq_eq_E8_coeff` is now **fully proved**: the entire Fourier coefficient + extraction (E₄ coeff = 240·σ₃, E₈ coeff = 480·σ₇, constant term 1, antidiagonal + `coeff_mul` split into 480·σ₃ boundary + 240²·convolutionLHS middle, then + `exact_mod_cast` ℂ→ℕ) is machine-checked, reducing it to `E4_sq_eq_E8_qExpansion`. + Computationally verified for n = 2, 3, 4 via `#eval`. + - `r8_via_sigma3`, `r8_one` are now **fully proved** after the `r8` definition + fix (`r8 n = 240·σ₃(n)` matching Θ_{E₈} = E₄, was incorrectly `480·σ₇`). - 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`, diff --git a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean index 6bc71ef5..98f07eb5 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/E8Sidon.lean @@ -164,35 +164,112 @@ Once Mathlib adds dim(M₈) = 1 or the valence formula, the sorry below becomes a one-line application. -/ +section ModularFormReduction + +open ModularForm EisensteinSeries ModularFormClass +open scoped CongruenceSubgroup + +/-- **The E₄² = E₈ q-expansion identity** — the single irreducible Mathlib gap. + + The q-expansion of the weight-4 Eisenstein series squared equals the + q-expansion of the weight-8 Eisenstein series. Equivalently `E₄² = E₈` as + modular forms for `SL(2,ℤ)`: both lie in `M₈(SL₂ℤ)`, which is + one-dimensional, and both have constant term 1, so they coincide. + + `TODO(lean-port)`: This is the *only* genuinely Mathlib-blocked step in the + whole E₄²=E₈ chain. Closing it requires `dim M₈(SL₂ℤ) = 1` (equivalently the + valence formula), which Mathlib v4.30.0-rc2 does not provide: + `Mathlib/NumberTheory/ModularForms/LevelOne.lean` proves `Module.rank` only + for weight ≤ 0 and carries an explicit + "TODO: Add finite-dimensionality of these spaces of modular forms", and + neither `Identities.lean` nor `Discriminant.lean` supplies an E₄/E₆/E₈ ring + relation. Once `dim M₈ = 1` lands this becomes a one-liner: `(E h4).mul (E h4)` + and `E h8` are both in the 1-dimensional `M₈` with equal constant term, hence + equal, and `qExpansion` (a ring hom) transports the equality. + + Everything downstream of this lemma — the entire coefficient extraction in + `E4_sq_eq_E8_coeff` below — is fully proved with no `sorry`. -/ +theorem E4_sq_eq_E8_qExpansion {h4 : (3 : ℕ) ≤ 4} {h8 : (3 : ℕ) ≤ 8} : + qExpansion 1 (E h4) * qExpansion 1 (E h4) = qExpansion 1 (E h8) := by + sorry + /-- The coefficient identity from E₄² = E₈. For n ≥ 2, the n-th Fourier coefficient of E₄² equals that of E₈: 480 · σ₇(n) = 480 · σ₃(n) + 240² · Σ_{m=1}^{n-1} σ₃(m) · σ₃(n-m) - This is equivalent to the classical identity of Eisenstein, proved via - the fact that M₈(SL₂ℤ) is one-dimensional and both E₄² and E₈ have - constant term 1. --/ + This is the classical Eisenstein identity. The proof extracts the n-th + q-expansion coefficient of both sides of `E4_sq_eq_E8_qExpansion`: the LHS + via `PowerSeries.coeff_mul` over the antidiagonal, whose boundary terms give + `2 · (1 · 240·σ₃(n))` and whose middle gives `240² · convolutionLHS n`; the + RHS gives `480·σ₇(n)` directly. All of this arithmetic is fully proved — the + only `sorry` is the modular-form identity `E4_sq_eq_E8_qExpansion`. -/ theorem E4_sq_eq_E8_coeff (n : ℕ) (hn : 2 ≤ n) : 480 * sigma7 n = 480 * sigma3 n + 240 ^ 2 * convolutionLHS n := by - -- TODO(lean-port): Blocked on Mathlib missing the valence formula or - -- dim M_8(SL₂ℤ) = 1. - -- - -- Proof path when available: - -- 1. Let E4 := EisensteinSeries.E (by norm_num : 3 ≤ 4) - -- 2. Let E8 := EisensteinSeries.E (by norm_num : 3 ≤ 8) - -- 3. Show E4.mul E4 - E8 is a weight-8 cusp form - -- 4. Apply valence_formula or dim_M8_eq_one to get E4² = E8 - -- 5. Extract n-th coefficient via qExpansion_eq_zero_iff and - -- PowerSeries.coeff_mul - -- 6. Simplify using E4_normalization, E8_normalization - -- - -- The coefficient identity then follows from comparing: - -- coeff n (qExpansion E₄²) = coeff n (qExpansion E₈) - -- ⟹ 240·σ₃(n) + 240²·conv(n) = 480·σ₇(n) (rearrange) - -- - -- Tracked in: this file, §4. - sorry + have h4 : (3 : ℕ) ≤ 4 := by norm_num + have h8 : (3 : ℕ) ≤ 8 := by norm_num + obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩ + -- E₄ q-expansion coefficient values + have c4 : ∀ j : ℕ, j ≠ 0 → + PowerSeries.coeff j (qExpansion 1 (E h4)) = 240 * (σ 3 j : ℂ) := by + intro j hj + rw [EisensteinSeries.E_qExpansion_coeff h4 (by decide) j, if_neg hj] + have hb : ((bernoulli 4 : ℚ) : ℂ) = -1 / 30 := by + rw [show bernoulli 4 = (-1 : ℚ) / 30 from by native_decide]; push_cast; ring + rw [hb]; push_cast; ring + have c40 : PowerSeries.coeff 0 (qExpansion 1 (E h4)) = (1 : ℂ) := by + rw [EisensteinSeries.E_qExpansion_coeff h4 (by decide) 0, if_pos rfl] + have c8 : PowerSeries.coeff (m + 1) (qExpansion 1 (E h8)) = 480 * (σ 7 (m + 1) : ℂ) := by + rw [EisensteinSeries.E_qExpansion_coeff h8 (by decide) (m + 1), if_neg (by omega)] + have hb : ((bernoulli 8 : ℚ) : ℂ) = -1 / 30 := by + rw [show bernoulli 8 = (-1 : ℚ) / 30 from by native_decide]; push_cast; ring + rw [hb]; push_cast; ring + -- convolution as a ℂ sum + have hconv : ((convolutionLHS (m + 1) : ℕ) : ℂ) + = ∑ k ∈ range m, (σ 3 (k + 1) : ℂ) * (σ 3 (m - k) : ℂ) := by + unfold convolutionLHS + rw [show (m + 1) - 1 = m from by omega, Finset.sum_map] + push_cast + apply Finset.sum_congr rfl + intro k hk + simp only [Function.Embedding.coeFn_mk, sigma3] + rw [show (m + 1) - (k + 1) = m - k from by omega] + -- the irreducible gap + have hq : qExpansion 1 (E h4) * qExpansion 1 (E h4) = qExpansion 1 (E h8) := + E4_sq_eq_E8_qExpansion + -- extract the (m+1)-th coefficient + have hcoeff : PowerSeries.coeff (m + 1) (qExpansion 1 (E h4) * qExpansion 1 (E h4)) + = PowerSeries.coeff (m + 1) (qExpansion 1 (E h8)) := by rw [hq] + rw [PowerSeries.coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk, c8] at hcoeff + -- evaluate the antidiagonal sum + have hS : (∑ k ∈ range (m + 1).succ, + PowerSeries.coeff k (qExpansion 1 (E h4)) * PowerSeries.coeff ((m + 1) - k) (qExpansion 1 (E h4))) + = 480 * (σ 3 (m + 1) : ℂ) + 240 ^ 2 * (convolutionLHS (m + 1) : ℂ) := by + rw [Nat.succ_eq_add_one, Finset.sum_range_succ, Finset.sum_range_succ'] + -- simplify the two boundary subtractions, then evaluate coeff 0 = 1, coeff (m+1) = 240·σ₃ + rw [show (m + 1) - (m + 1) = 0 from by omega, show (m + 1) - 0 = m + 1 from by omega, + c40, c4 (m + 1) (by omega)] + -- middle sum + have hmid : (∑ k ∈ range m, + PowerSeries.coeff (k + 1) (qExpansion 1 (E h4)) * PowerSeries.coeff ((m + 1) - (k + 1)) (qExpansion 1 (E h4))) + = 240 ^ 2 * ∑ k ∈ range m, (σ 3 (k + 1) : ℂ) * (σ 3 (m - k) : ℂ) := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro k hk + rw [Finset.mem_range] at hk + rw [show (m + 1) - (k + 1) = m - k from by omega, + c4 (k + 1) (by omega), c4 (m - k) (by omega)] + ring + rw [hmid, hconv] + ring + rw [hS] at hcoeff + -- hcoeff : 480·σ3 + 240²·conv = 480·σ7 (in ℂ) + have hCfinal : (480 : ℂ) * (σ 7 (m + 1)) = 480 * (σ 3 (m + 1)) + 240 ^ 2 * (convolutionLHS (m + 1)) := + hcoeff.symm + simp only [sigma7, sigma3] + exact_mod_cast hCfinal + +end ModularFormReduction -- Computational verification for small n -- These witnesses confirm the identity holds for specific values @@ -287,36 +364,31 @@ theorem sidon_energy_bound (S : Finset ℕ) (hS : IsSidonSet S) : /-- The E₈ lattice theta series coefficient r₈(n) counts the number of vectors in E₈ of squared norm 2n. The first few values are: - r₈(0) = 1, r₈(1) = 240, r₈(2) = 2160, r₈(3) = 6720, ... -/ + r₈(0) = 1, r₈(1) = 240, r₈(2) = 2160, r₈(3) = 6720, ... + + The theta series of the E₈ root lattice is Θ_{E₈} = E₄ (Conway–Sloane, + Ch. 4 §6), the normalized weight-4 Eisenstein series, so the n-th + coefficient (n ≥ 1) is 240·σ₃(n). We define `r8` directly from this + theta-series normalization. (Note: 480·σ₇ are the coefficients of the + weight-8 Eisenstein series E₈ — a *different* modular form — and must + not be used here; that conflation is what the E₄² = E₈ identity relates.) -/ def r8 (n : ℕ) : ℕ := - if n = 0 then 1 else 480 * sigma7 n + if n = 0 then 1 else 240 * sigma3 n -/-- r₈ matches the E₈ theta series: Θ_{E₈} = E₄ (a classical result). - The theta series of E₈ equals the normalized Eisenstein series of weight 4, -- TODO(wolfram-verify): classical Θ_{E₈} = E₄ identity - so r₈(n) for n ≥ 1 equals 240 · σ₃(n). - - Wait — this uses E₄, not E₈. The identity Θ_{E₈} = E₄ is itself a - consequence of E₄ being the unique modular form of weight 4 with - constant term 1. The r₈ function above uses the E₈ normalization - (480 · σ₇) which equals 240 · σ₃ + 240² · conv by the E₄² = E₈ identity. --/ +/-- r₈ matches the E₈ theta series: Θ_{E₈} = E₄ (Conway–Sloane, Ch. 4 §6). + The theta series of the E₈ root lattice equals the normalized weight-4 + Eisenstein series E₄, so its n-th coefficient (n ≥ 1) is 240·σ₃(n). + Since `r8` is defined directly from this theta-series normalization, + the identity holds definitionally once the n = 0 branch is excluded. -/ theorem r8_via_sigma3 (n : ℕ) (hn : 1 ≤ n) : r8 n = 240 * sigma3 n := by - -- TODO(lean-port): This follows from Θ_{E₈} = E₄, which requires the - -- same dimension argument as E₄² = E₈. Specifically: - -- Θ_{E₈} is a modular form of weight 4 for SL₂ℤ with constant term 1. - -- E₄ is the unique such form (dim M₄ = 1). - -- Therefore Θ_{E₈} = E₄, giving r₈(n) = 240·σ₃(n) for n ≥ 1. - sorry + unfold r8 + rw [if_neg (by omega)] -/-- The E₈ lattice has 240 minimal vectors (roots). -/ +/-- The E₈ lattice has 240 minimal vectors (roots): r₈(1) = 240·σ₃(1) = 240. -/ lemma r8_one : r8 1 = 240 := by - simp [r8, sigma7] - -- 480 * σ₇(1) = 480 * 1 = 480 ≠ 240 — note: r₈(1) = 240 but our definition - -- uses the E₈ Eisenstein normalization. This shows the definition should use - -- E₄ coefficients, not E₈. The E₄² = E₈ identity reconciles them. - -- TODO(lean-port): fix definition to use Θ_{E₈} = E₄ directly - sorry + rw [r8_via_sigma3 1 (le_refl 1)] + native_decide -- ═══════════════════════════════════════════════════════════════════════════════ -- §8. Greedy Sidon Extraction and Collision Theory @@ -730,11 +802,9 @@ theorem greedy_sidon_sqrt (S : Finset ℕ) (hS : IsSidonSet S) : from σ₃(n) growth. -/ theorem e8_levelset_density (N : ℕ) (hN : 1 ≤ N) : ∃ C : ℕ, ∀ n, 0 < n → n ≤ N → r8 n ≤ C * n ^ 3 := by - -- We use the crude bound: σ₇(n) ≤ n * n⁷ = n⁸ (each of ≤n divisors is ≤n⁷). - -- Then r8 n = 480 * σ₇(n) ≤ 480 * n⁸ = 480 * n⁵ * n³ ≤ 480 * N⁵ * n³. - -- Take C = 480 * N ^ 5 + 1 (the +1 handles the constant term). - -- Simpler: since N is finite, take C = sup of {r8(n) | 1 ≤ n ≤ N} + 1. - -- Even simpler: the Finset.sup over Icc 1 N of r8 gives a finite max. + -- Since r8 n = 240·σ₃(n) and σ₃(n) = O(n³), r8 grows like n³. We avoid the + -- asymptotic bound entirely: N is finite, so the Finset.sup over Icc 1 N of + -- r8 gives a finite max C, and r8 n ≤ C = C·1 ≤ C·n³ for every n ≥ 1. use (Finset.Icc 1 N).sup' ⟨N, Finset.mem_Icc.mpr ⟨hN, le_refl N⟩⟩ r8 intro n hn hnN have hmem : n ∈ Finset.Icc 1 N := Finset.mem_Icc.mpr ⟨hn, hnN⟩ @@ -933,17 +1003,23 @@ theorem fiber_partition (S : Finset ℕ) (s : ℕ) : | `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 | +| `E4_sq_eq_E8_coeff` | §4 | Full proof: q-expansion coeff extraction from E4_sq_eq_E8_qExpansion | +| `r8_via_sigma3` | §7 | Full proof: r8 normalized to 240·σ₃ (Θ_{E₈} = E₄) | +| `r8_one` | §7 | Full proof: r8 1 = 240·σ₃(1) = 240 | -### Sorry inventory (6 sorry tokens across 6 theorems, all with TODO(lean-port)) +### Sorry inventory (4 sorry tokens across 4 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₄ | +| `E4_sq_eq_E8_qExpansion` | §4 | Mathlib: dim M₈(SL₂ℤ) = 1 / valence formula (absent in v4.30) | | `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 | + +The `E4_sq_eq_E8_coeff` identity is now fully reduced: the entire Fourier +coefficient extraction is machine-checked, and the only residual `sorry` is the +single modular-form identity `E4_sq_eq_E8_qExpansion` (E₄² = E₈ as q-expansions), +which is exactly the one fact Mathlib v4.30 is missing. -/ end Semantics.E8Sidon