Decision: how to build the operator bridge for the T² index (Route A vs B)

[mrdouglasny]

We have a genuine direction choice to make before the next index-pairing build, and it touches both our efforts — opening this to decide and divide labor. Full scope: docs/INDEX_PAIRING.md (PR #13).

Where we are

• Function-theoretic geometric count — done (on main): dim H⁰(L_k) = k (holSection_finrank_eq, M3a) and H¹(L_k) = 0 (holSectionNeg_eq_bot, M3b), via the contour shift + Fourier recursion + Parseval — no index theorem, no L².
• Model — done: fredholmIndex_magneticDirac = k (the ℓ²(ℕ)⊗ℂᵏ Landau model, with magnetic translations).
• Operator side — done (your WIP: Fredholm operators for the index pairing (Riesz–Schauder in progress) #11): compact operators + Riesz–Schauder Fredholm half ⇒ index(D⁺) is well-defined (finite-dim ker/coker) once D⁺ has compact resolvent.

What's missing is the bridge: that the genuine operator D⁺ on L²(L_k) has index = k. The Fredholm property gives well-definedness; the value still needs an identification of ker D⁺ with what we counted.

The choice

Both routes have a real Mathlib gap:

• Route A — Weyl's lemma / elliptic regularity for ∂̄. ker D⁺ ⊆ L² weak solutions ⇒ holomorphic ⇒ = H⁰(L_k) (= k by M3a). Mathlib has no hypoellipticity / elliptic regularity at all → effectively blocked.
• Route B — Landau/Hermite decomposition (recommended). L²(L_k) ≅ ⨁ₙ ℂᵏ via Hermite-Gaussian eigenfunctions ⇒ D⁺ ≅ magneticDirac k, transporting the formalized model index = k. Gap: Mathlib has only Hermite polynomials + Rodrigues, not the L²(ℝ) orthonormal basis.

Either way M1 (the weighted L²(L_k) sections + the twisted ∂̄) is a from-scratch build.

Proposed plan (to confirm)

1. Recommend Route B. First concrete, reusable step: build the Hermite orthonormal basis of L²(ℝ) (gating lemma; a clean Mathlib-gap fill).
2. Then M1 (weighted L²(L_k)), the magnetic guiding-center reduction, and D⁺ ≅ magneticDirac k.

Coordination question

• Route A or B? (I lean B.)
• Division of labor: your WIP: Fredholm operators for the index pairing (Riesz–Schauder in progress) #11 (Riesz–Schauder) gives the Fredholm well-definedness; happy to take the Hermite L² basis + M1, or split differently — what works for you?
• Anything in your Fredholm direction that changes the recommended route?

🤖 Generated with Claude Code

[JonBannon]

Went with Route B. We can of course build out the machinery for A later. Most of this stuff will have to be reworked if it will go into Mathlib, of course. Having this codebase will be very helpful even in the initial state, though.