CLAIMS_STATUS.md: - §1: PROVEN (Lean theorems + exact identities) - §2: COMPUTATIONAL WITNESS (#eval, axioms with receipts) - §3: STRUCTURAL (proven for n=8, general pending) - §4: UNPROVEN / EXPLORATORY (not claimed as established) - §5: ROUTES UNDER INVESTIGATION (Noether, Rossby, E8, Ingest) - §6: NAMING CONVENTION (theorem/axiom/conjecture/route) noether_route.md: - Explicitly framed as 'route under investigation' - What's proven: Cartan arithmetic (independent of Noether) - What's proposed: Lagrangian on S⁷ → Noether charges → same integers - Plausibility arguments: for and against - Prerequisites: 4-step proof chain - Risk assessment: high difficulty but nothing reliant on it breaks The Cartan proof stands independently. Noether is a possible deepening, not a retroactive justification.
4.1 KiB
Noether Route — S⁷ Lagrangian Hypothesis
Status: ROUTE UNDER INVESTIGATION — not claimed as established
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.