From b482b927dedef4d2a26043883118597d78cf06bc Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sun, 21 Jun 2026 17:25:49 -0400 Subject: [PATCH] Sync blueprint and roadmap doc with HermiteL2.lean (PR #16) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Gaussian-weighted Hermite orthogonality landed on main without blueprint coverage. Add Section 3.8 documenting derivative_hermite, integrable_aeval_mul_gaussian, hermite_integral_eq_zero_of_ne, hermite_integral_self, and hermite_orthogonality, framed as the first half of the Route B gating lemma (Hermite L²(R) basis) from INDEX_PAIRING.md's M3c/M1/M4 operator-bridge roadmap. Also update INDEX_PAIRING.md's progress tracker and Mathlib-inventory table to reflect that the orthogonality half is done, with normalization + completeness still open. Co-Authored-By: Claude Sonnet 4.6 --- SpectralTriples/docs/INDEX_PAIRING.md | 19 ++++++-- blueprint/src/content.tex | 68 ++++++++++++++++++++++++++- 2 files changed, 81 insertions(+), 6 deletions(-) diff --git a/SpectralTriples/docs/INDEX_PAIRING.md b/SpectralTriples/docs/INDEX_PAIRING.md index 0dc67bf..78229d9 100644 --- a/SpectralTriples/docs/INDEX_PAIRING.md +++ b/SpectralTriples/docs/INDEX_PAIRING.md @@ -203,10 +203,19 @@ remain substantial — this is a multi-step analytic build, not a single lemma. - **M3c / M1 / M4 — the operator bridge** (detailed scope above): connect the operator `ker D⁺ ⊆ L²(L_k)` to the counted sections. Both routes have real Mathlib gaps — Route A (Weyl's lemma) is fully absent; Route B (Landau/Hermite, recommended) needs the Hermite `L²(ℝ)` - basis (absent) plus the weighted `L²(L_k)` space (M1, from scratch). **Recommended first step: - the Hermite orthonormal basis of `L²(ℝ)`** — the gating lemma for Route B, a clean reusable - Mathlib-gap fill. Jon's merged Riesz–Schauder (#11) supplies the Fredholm *well-definedness*; - the *value* `= k` still needs this bridge. + basis (started, see below) plus the weighted `L²(L_k)` space (M1, from scratch). Jon's merged + Riesz–Schauder (#11) supplies the Fredholm *well-definedness*; the *value* `= k` still needs + this bridge. + - **Hermite orthogonality — done** (`SpectralTriples.HermiteL2`, PR #16): the gating lemma for + Route B is the Hermite-function orthonormal basis of `L²(ℝ)`; this is its first half, the + Gaussian-weighted orthogonality of the Hermite *polynomials* + `∫ Hₘ Hₙ e^{-x²/2} = n!√(2π)·δₘₙ` (`hermite_orthogonality`), proved without `n`-fold + integration by parts via the derivative recursion `Hₙ₊₁' = (n+1)·Hₙ` + (`derivative_hermite`) and a single integration by parts. Sorry-free, axiom-clean. + - **Still TODO for the Hermite basis**: the normalization constants `cₙ` (so that + `hₙ = cₙ·Hₙ·e^{-x²/2}` is unit norm in `L²(ℝ)`) and completeness of `{hₙ}` in `L²(ℝ)` + (needed to package it as a Mathlib `HilbertBasis`) — via density of polynomials-times-Gaussian + or the spectral theory of the Hermite/oscillator operator. ## Mathlib inventory (for the bridge) @@ -214,7 +223,7 @@ remain substantial — this is a multi-step analytic build, not a single lemma. |---|---| | Jacobi theta functions `jacobiTheta₂(z, τ)` | ✅ `Mathlib.NumberTheory.ModularForms.JacobiTheta` | | Gaussian integrals; Hermite *polynomials* + Rodrigues formula | ✅ present (`RingTheory/Polynomial/Hermite`) | -| Hermite *functions* as an `L²(ℝ)` orthonormal basis (gating M4 / Route B) | ❌ **build** (only polynomials present) | +| Hermite *functions* as an `L²(ℝ)` orthonormal basis (gating M4 / Route B) | 🟡 **in progress** — Gaussian-weighted orthogonality done (`HermiteL2.lean`); normalization + `L²` completeness remain | | theta functions *with characteristics*; the count `dim H⁰(L_k)=k`, `H¹=0` | ✅ **done** (`FourierHolomorphic`: `holSection_finrank_eq`, `holSectionNeg_eq_bot`) | | `L²` sections of a line bundle / weighted quasi-periodic `L²` (M1) | ❌ build by hand | | elliptic regularity / Weyl's lemma for `∂̄` (Route A) | ❌ absent — use Route B instead | diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 1968694..68d3952 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -361,7 +361,10 @@ \chapter{Examples} connect the abstract flux-$k$ model of Section~\ref{sec:magnetic-dirac} back to genuine geometry: together they give a complete, purely algebraic dimension count $\dim H^0(L_k) = k$, $\dim H^1(L_k) = 0$ for the degree-$k$ line bundle on the square torus, -with no index theorem and no $L^2$ analysis. +with no index theorem and no $L^2$ analysis. Section~\ref{sec:hermite-l2} begins the +remaining operator bridge (M3c/M1/M4): the Gaussian-weighted orthogonality of the Hermite +polynomials, the foundation of the Hermite-function $L^2(\mathbb{R})$ basis needed for the +Landau/Hermite decomposition route. \section{Block-diagonal operators on \texorpdfstring{$\ell^2$}{l2}} \label{sec:diagonal-operators} @@ -871,3 +874,66 @@ \section{The Fourier-coefficient recursion: an exact dimension count} Lemma~\ref{lem:holCoeff-tendsto-atTop-zero} unless every coefficient is already $0$, and then Theorem~\ref{thm:eq-zero-of-holCoeff-eq-zero} gives $f = 0$. \end{theorem} + +\section{The Hermite functions: Gaussian-weighted orthogonality} +\label{sec:hermite-l2} + +\textbf{Status: partial (orthogonality only).} This section is the foundation of \emph{Route +B} for the M3c/M1/M4 operator bridge of Section~\ref{sec:fourier-holomorphic} (see +\texttt{SpectralTriples/docs/INDEX\_PAIRING.md}): the recommended next step there is to build +the Hermite \emph{functions} $h_n(x) = c_n \cdot H_n(x) \cdot e^{-x^2/2}$ as an orthonormal +basis of $L^2(\mathbb{R})$, the gating lemma for the Landau/Hermite decomposition that +identifies the geometric magnetic Dirac operator with the already-formalized model +(Section~\ref{sec:magnetic-dirac}). Mathlib has the probabilists' Hermite \emph{polynomials} +and the Rodrigues identity, but neither the Gaussian-weighted orthogonality integral nor the +$L^2$ basis. This section proves the orthogonality integral; the normalization constants $c_n$ +and the completeness of $\{h_n\}$ in $L^2(\mathbb{R})$ (needed for the \texttt{HilbertBasis}) +remain to be built. + +\begin{lemma}[Hermite derivative identity] + \label{lem:derivative-hermite} + \lean{Polynomial.derivative_hermite} + \leanok + The probabilists' Hermite polynomials satisfy $H_{n+1}' = (n+1) \cdot H_n$. (Mathlib has the + three-term recursion $H_{n+1} = X H_n - n H_{n-1}$ but not this derivative form.) +\end{lemma} + +\begin{lemma}[Integrability against the Gaussian weight] + \label{lem:integrable-aeval-mul-gaussian} + \lean{Polynomial.integrable_aeval_mul_gaussian} + \leanok + Any polynomial $p$ times the Gaussian weight $e^{-x^2/2}$ is integrable on $\mathbb{R}$. +\end{lemma} + +\begin{theorem}[Off-diagonal orthogonality] + \label{thm:hermite-integral-eq-zero-of-ne} + \lean{Polynomial.hermite_integral_eq_zero_of_ne} + \leanok + \uses{lem:derivative-hermite, lem:integrable-aeval-mul-gaussian} + For $m \neq n$, $\int_{\mathbb{R}} H_m(x) H_n(x) e^{-x^2/2}\,dx = 0$. From the Rodrigues + identity $(H_n \cdot w)' = -H_{n+1} \cdot w$ (with $w = e^{-x^2/2}$) and a single integration + by parts, the weighted pairing of a polynomial $P$ against $H_{n+1}$ satisfies + $\langle P, H_{n+1}\rangle = \langle P', H_n\rangle$; iterating shows $\deg P \leq n$ forces + $\langle P, H_{n+1}\rangle = 0$, which gives off-diagonal vanishing without $n$-fold + integration by parts. +\end{theorem} + +\begin{theorem}[Diagonal value] + \label{thm:hermite-integral-self} + \lean{Polynomial.hermite_integral_self} + \leanok + \uses{lem:derivative-hermite, thm:hermite-integral-eq-zero-of-ne} + $\int_{\mathbb{R}} H_n(x)^2 e^{-x^2/2}\,dx = n! \sqrt{2\pi}$. The same integration-by-parts + recursion gives $\langle H_{n+1}, H_{n+1}\rangle = (n+1) \langle H_n, H_n \rangle$ + (Lemma~\ref{lem:derivative-hermite}), reducing to the base case + $\int_{\mathbb{R}} e^{-x^2/2}\,dx = \sqrt{2\pi}$ (the Gaussian integral). +\end{theorem} + +\begin{theorem}[Gaussian-weighted orthogonality] + \label{thm:hermite-orthogonality} + \lean{Polynomial.hermite_orthogonality} + \leanok + \uses{thm:hermite-integral-eq-zero-of-ne, thm:hermite-integral-self} + $\int_{\mathbb{R}} H_m(x) H_n(x) e^{-x^2/2}\,dx = n! \sqrt{2\pi} \cdot \delta_{mn}$, combining + the off-diagonal and diagonal cases. +\end{theorem}