3 The harmonic oscillator
HarmonicOscillator/, on top of Systems/Fock/, read in the order the physics unfolds.
3.1 Schwartz space
Physlib’s position/momentum operators, recombined into \(a_i,a_i^\dagger \) on Schwartz space \(\mathcal S(\mathbb R^d,\mathbb C)\), for oscillator strength \(\kappa {\gt}0\).
\([a_i,a_j^\dagger ] = \delta _{ij}\), proved from Physlib’s underlying \([\mathbf x,\mathbf p]\) relation, not assumed.
physlibA/physlibAc packaged as a genuine LadderSystem (Definition 10) on \(\mathcal S(\mathbb R^d,\mathbb C)\).
3.2 Spectrum: the one analytic admission
\(\mathbf x,\mathbf p\) (hence physlibA/physlibAc) are mutually adjoint w.r.t. the genuine \(L^2\) pairing on Schwartz space — standard textbook physics (integration by parts for \(\mathbf p\); \(\mathbf x\) is literally multiplication by a real function). Not yet proved here or in Physlib: Physlib proves position’s self-adjointness on the actual \(L^2\) Hilbert space but leaves momentum’s as an explicit TODO, and neither is yet transported to this bounded Schwartz-space picture.
Standard real-analysis (positivity of \(\int |f|^2\) over a nonempty open set), not built elsewhere in this project.
3.3 The Hamiltonian
\(H := \hbar \omega (N + d/2)\), for any LadderSystem (generic Fock content, not specific to the physical oscillator despite living in the HarmonicOscillator/ folder).
With \(\hbar \omega \neq 0\) and Fock-completeness, \(\mathrm{eigenspace}(H,\hbar \omega (n+d/2)) = \mathrm{vacuumSpan}(L,\Omega ,n)\).
3.4 Classification and quantum numbers
\(\mathrm{vacuumSpan}(L,\Omega ,n)\) is an irreducible \(\mathfrak {gl}(d)\)-module. Blocked on a still-missing type-\(A_{d-1}\) classical-family root datum for \(\mathfrak {gl}(d)/\mathfrak {sl}(d)\) at general rank (Mathlib has none; this project has only built the rank-\(1\) case). Admitted directly here, not routed through Theorem 7 — the docstring is explicit that plumbing through the full CyclicHighestWeightData apparatus is real, system-specific work not attempted in this pass, unlike Hydrogen/Classification.lean’s Theorem 49, which does make that call for real. Closing this admission by routing it through Theorem 7 the way Hydrogen already does is the natural next step.
Given \(d{\gt}0\) modes and nonzero coupling, the excitation-number sectors assemble into a genuine Foundations.SpectralSector of the algebraic Hamiltonian.
\(E_{ii}\) restricted to \(\mathrm{vacuumSpan}(L,\Omega ,n)\) — playing the same role SoSystem.cartanGen (Theorem 22) plays for \(\mathfrak {so}(n{+}1)\).
A one-line corollary of Theorem 11: \([E_{ii},E_{jj}]\) collapses to \(0\) whether or not \(i=j\).
Standard, not otherwise attacked here. Mirrors Theorem 51’s admission for \(\mathfrak {so}(n{+}1)\) exactly — the two systems’ matching admissions for the matching role in the same shared construction.
3.5 Summary leaves
HarmonicOscillator/Summary.lean item 4: a direct citation, zero new proof content.
HarmonicOscillator/Summary.lean item 9.