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.
4.6 KiB
⛔ DEAD — Noether Route (3 fatal math errors)
Status: DEAD (June 30, 2026). Adversarial review found:
- S⁷ is the wrong configuration space (discrete crossStep, not continuous flow)
- No subgroup of S⁷ has 8 generators (strand count ≠ Lie group dimension)
- 17 broken generators from a 6-dim group is dimensionally impossible
Replaced by: Cartan connection route — already proven in CartanConnection.lean (Jacobiator_basis_all, gate_C_d_CE_mu_zero).
Do not cite this route.
(Original content below, preserved for archival)
Noether Route — S⁷ Lagrangian Hypothesis (DEAD)
References: docs/CLAIMS_STATUS.md, formal/CoreFormalism/HopfFibration.lean
What's Proven
The spectral gap ∆ = 17/1792 is an exact rational identity derived from:
- σ = 39/256 (Cartan weight matrix spectral radius for 8-strand braid)
- τ = 1/7 (Sidon doubling threshold, n−1 = 7)
- D = lcm(256, 7) = 1792
- p = 39 × 7 − 256 × 1 = 17
This is structural — it follows from the Cartan integers and the Sidon doubling count. It does NOT require a Lagrangian, Noether charges, or symmetry breaking. It's exact arithmetic on the underlying combinatorics.
What This Route Proposes
That these same numbers (39, 256, 7, 17, 1792, 28) could ALSO emerge from a Noether-theoretic construction:
Lagrangian ℒ on total space S⁷ of quaternionic Hopf fibration
├── SU(2) × SU(2) gauge symmetry (8 generators)
├── Noether 1st theorem → 8 conserved currents → Cartan charge spectrum
├── ℤ₇ discrete symmetry (Sidon doubling periodicity)
├── Common denominator D = lcm(|G_continuous|, |G_discrete|) = 1792
└── Broken generators = 17 (gap numerator)
Plausibility
Arguments for:
- The quaternionic Hopf fibration S³ → S⁷ → S⁴ HAS a natural SU(2) gauge symmetry (the fiber is SU(2))
- The Cartan decomposition of the braid crossing matrix produces exactly the same integers (39, 256, 273) that would appear in a Noether charge computation
- The Sidon doubling group ℤ₇ IS a discrete subgroup of the U(1) ⊂ SU(2) fiber, so the common denominator D = lcm(256, 7) has a group-theoretic interpretation
- The number 17 = 273 − 256 could represent broken Noether generators (those that don't survive the Cartan → Sidon projection)
Arguments against:
- No Lagrangian on S⁷ has been explicitly constructed or verified in this framework
- The Cartan weight matrix is derived combinatorially (braid crossing counts), not from a variational principle
- "Broken generators" is a physical interpretation, not a mathematical proof — the 17 could have other explanations
- Noether's second theorem (gauge symmetries → Bianchi identities) hasn't been checked against the braid dynamics
What Would Make This Route Viable
A proof that:
- There exists a Lagrangian density ℒ on S⁷ whose Euler-Lagrange equations produce the braid crossing dynamics
- The Noether current associated with SU(2) fiber symmetry produces conserved charges matching the Cartan integers
- The discrete ℤ₇ symmetry corresponds to the Sidon doubling operation
- The broken Noether generator count equals 17
Prerequisites (Next Steps)
□ Construct explicit Lagrangian ℒ on S⁷
- Use the quaternionic structure (a,b,c,d) ∈ S⁷ already in HopfFibration.lean
- Require SU(2) gauge invariance
- Require ℤ₇ periodicity condition
□ Verify Euler-Lagrange equations reduce to braid crossing dynamics
- Compare with existing crossStep in BraidStateN.lean
- Check that eigensolid fixed point = extremum of ℒ
□ Compute Noether charge spectrum
- Use Cartan decomposition on the 8 SU(2)×SU(2) generators
- Verify that the surviving charges produce the integer a = 39
□ Count broken generators
- Verify that a − 2ⁿ × τ = 39 − 256/7, after rationalization, gives 17
Risk Assessment
- High: This is a new formalization with no existing Lean infrastructure for Lagrangian mechanics on the Hopf fibration
- Medium: The integers already match; the question is whether the derivation path is Lagrangian → Cartan or Cartan → Lagrangian
- Low: If the route FAILS, nothing in the existing formalization breaks — the gap 17/1792 is proven independently
Bottom line: This route is a legitimate investigation. It does NOT retroactively require the existing results to depend on Noether's theorem. The Cartan proof stands on its own. This route asks whether the SAME integers admit an additional (Noether-theoretic) provenance, which would deepen but not replace the existing proof.