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

fix(lean): reduce E4_sq_eq_E8_coeff to single modular-form q-expansion gap

Browse source 
Fully prove the E4^2=E8 Fourier coefficient identity (E4_sq_eq_E8_coeff) modulo one isolated, honestly-named Mathlib gap.

- Add E4_sq_eq_E8_qExpansion: the lone irreducible step (E4^2=E8 as q-expansions). Blocked on dim M8(SL2Z)=1 / valence formula, absent in Mathlib v4.30 (LevelOne.lean proves Module.rank only for weight <= 0).
- Machine-check the entire coefficient extraction for E4_sq_eq_E8_coeff: E4 coeff = 240*sigma3, E8 coeff = 480*sigma7, constant term 1, antidiagonal coeff_mul split into 480*sigma3 boundary + 240^2*convolutionLHS middle, then exact_mod_cast C->N. Previously a single hand-waved sorry.
- Wrap in section ModularFormReduction with local opens (ModularForm EisensteinSeries ModularFormClass) to avoid name clashes.
- Update AGENTS.md + .cursorrules: E8Sidon sorry inventory 6 -> 4.

E8Sidon sorries now: E4_sq_eq_E8_qExpansion (Mathlib-blocked), collision_excess_decrease, greedy_sidon_extraction, e8_singer_improvement.

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-16 01:19:06 +00:00
parent 5cacb86ddb
commit ca422d43b7
3 changed files with 149 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
.cursorrules
View file

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

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

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

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

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