Remove rossby_e8_completion_roadmap.md

docs/rossby_e8_completion_roadmap.md

@@ -1,61 +0,0 @@
-# Rossby Energy + E8 Sidon — Completion Roadmap
-
-## Current State
-
-### Rossby Energy (BraidStateN.lean)
-- ✅ `crossingEnergy` — defined (Q16_16 weighted phase sum)
-- ✅ `rossby_convergence_bound` — proven (step count increases)
-- ⚠️ `rossby_energy_monotone` — axiom (energy decreases under crossStep)
-- ⚠️ `regime_classification` — trivial (28 = C(8,2) coupling pairs)
-- ❌ `crossingEnergy_invariant` — not yet defined
-- ❌ `rossby_faster_than_kelvin` — not yet defined
-
-### E8 Sidon (E8Sidon.lean)
-- ✅ `sigma3`/`sigma7` — defined
-- ✅ `E8LevelSet` — defined
-- ⚠️ `sigma3_multiplicative` — 1-line fix (blocked on Mathlib `Nat.divisors_mul`)
-- ⚠️ `e8_levelset_sidon` — computational N≤200, structural blocked
-- ❌ `erdos30_bound` — not yet computed
-
-## Completion Paths
-
-### Phase 1: Rossby Energy (n=8, computational)
-
-```
-Step 1.1: Define a concrete test state (8-strand with specific chiral labels)
-Step 2.1: Compute crossingEnergy(s) and crossingEnergy(crossStep(s))
-Step 3.1: native_decide the difference (16-20 Q16_16 comparisons)
-Step 4.1: Extract #eval witness to rossby_energy_decrease
-```
-
-**Goal**: One computational receipt proving energy decreases for a concrete Rossby (chiral) state vs staying constant for a Kelvin (achiral) state.
-
-### Phase 2: E8 Sidon (N≤200, computational)
-
-```
-Step 2.1: Unblock sigma3_multiplicative:
-  import Mathlib.Data.Nat.Divisors
-  Use Nat.divisors_mul (a * b) (ha : a ≠ 0) (hb : b ≠ 0) (hcop : Coprime a b)
-  → key lemma: sum over divisors of product = product of sums
-
-Step 2.2: Build concrete level sets for N=8, 16, 32, 64, 128
-  For each N, compute σ₃(n) for n ≤ N via native_decide
-  Verify pairwise sums are unique (Sidon property)
-
-Step 2.3: Extract #eval witness:
-  #eval e8_levelset_sidon 64
-  → output: "Sidon verified for N=64 (σ₃ constraint)"
-```
-
-### Phase 3: Integration — Rossby ↔ E8 Sidon bridge
-
-The 28 coupling pairs (C(8,2) combinatorial) bound the possible crossing configurations.
-The E8 Sidon construction improves the density bound.
-Together: ε ≥ 1/4 with at most 28 iteration patterns.
-
-### Phase 4: Generalization (future work)
-
-- `sigma3_multiplicative` → full Mathlib dependency → PR upstream
-- Dickman function density estimates → smooth number theory
-- CrossStep contractiveness → needs Q16_16 inequality lemmas
-- `rossby_faster_than_kelvin` → needs comparison lemma for energy dissipation rates