mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00

allaun 6486b89384 fix(review): angry reviewer corrections — retract consistently across all files

BraidStateN.lean: fix π₀(Diff⁺(S⁶)) → Θ₇, note retraction
HopfFibration.lean: fix comment, remove diffeomorphism claim
CLAIMS_STATUS.md: move π₀ claim to retracted, mark Noether as dead

Retraction headers added to:
- hopf_portability_criterion.md: ⛔ RETRACTED header
- hopf_ingest_bridge.md: ⛔ RETRACTED header (depends on retracted criterion)
- noether_route.md: ⛔ DEAD header (3 fatal math errors)

rotational_wave_braid_correspondence.md: fix 28 = C(8,2), remove π₀ claim
rossby_e8_completion_roadmap.md: fix coupling pairs language

Cleanup: no file still claims π₀(Diff⁺(S⁶)) ≅ ℤ₂₈ as true.

2026-06-30 20:19:12 -05:00

2.4 KiB

Raw Blame History

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

2.4 KiB Raw Blame History