Overview
What this is.
This blueprint tracks the current source tree, not an aspirational one: every \lean{} tag below is checked by leanblueprint checkdecls against the actual compiled project, so a stale name breaks the build rather than silently lying. Every node carries \leanok if and only if the Lean declaration it names is fully proved, no sorry — nodes without it are declarations that exist (the statement is real, checkdecls confirms it) but are currently admitted. That distinction, drawn automatically by the dependency-graph renderer rather than asserted by hand in prose, is the whole point of using this tool instead of a hand-written document.
The shape.
Two physical systems, read the same way: an analytic entry point (concrete Schwartz-space operators from Physlib) \(\to \) one or two analytic admissions \(\to \) the same Foundations theorems, invoked at each system’s own concrete data \(\to \) a Summary.lean leaf that cites everything with no new proof content. General spatial dimension is the primary story for the hydrogen atom (§4, hidden symmetry \(\mathfrak {so}(n{+}1)\), any \(n\)); the classical \(d=3\) case, where the exceptional isomorphism \(\mathfrak {so}_4\cong \mathfrak {so}_3 \oplus \mathfrak {so}_3\) holds, is a secondary, highlighted exceptional case (§5), kept because it is the textbook result, not because it is the target.
Chapter 1, Foundations — the shared backend both physical systems literally call: the labeled-decomposition constructor (Foundations/QuantumNumberScheme.lean) and the highest-weight/Weyl boundary (Foundations/WeylTheory/HighestWeightModule.lean, Foundations/WeylTheory/WeylCharacter.lean). This is where every deliberate general-level admission in the whole project lives.
Chapter 2, System structures — physics-free machinery each physical system instantiates: the bosonic CCR/Fock engine (Systems/Fock/), the \(\mathfrak {sl}_2\)/angular-momentum engine and its commuting-pair classification (Systems/Sl2/), and the orthogonal-Lie-algebra engine (Systems/Orthogonal/).
Chapter 3, The harmonic oscillator — HarmonicOscillator/, read start to finish: SchwartzSpace.lean \(\to \) Spectrum.lean \(\to \) Hamiltonian.lean \(\to \) WeylClassification.lean \(\to \) QuantumNumbers.lean \(\to \) Summary.lean.
Chapter 4, The hydrogen atom, general dimension — Hydrogen/, the primary story, the identical shape: HydrogenSoData.lean \(\to \) SchwartzSpace.lean \(\to \) Spectrum.lean \(\to \) Classification.lean \(\to \) QuantumNumbers.lean \(\to \) Summary.lean.
Chapter 5, The exceptional case \(d=3\) — Hydrogen/Exceptional/, the classical \(\mathfrak {so}_4\) route, secondary.
On admissions (“sorries”).
Every admitted fact below is a standalone, honestly-named theorem, consumed unconditionally by whatever needs it — never a caller-supplied hypothesis threaded through a theorem signature so that it merely looks proved. See each admission’s node for exactly what it asserts, why it is not yet proved, and (via the dependency graph) exactly what depends on it. SORRIES.md at the repository root gives the same information in prose form, cross-referenced against exact file/line locations, if a table is more convenient than the graph.
A note on Physlib.
Physlib.QuantumMechanics.Hydrogen.Basic and .../LaplaceRungeLenzVector.lean already define the (regularized) hydrogen Hamiltonian and Runge–Lenz operator on Schwartz space and prove most of their commutation relations; its own module documentation lists the bound-state point spectrum as an open TODO. Chapter 4 below is wired directly to these concrete operators (unlike an earlier version of this project, kept now only in git history, which used a fully decoupled algebraic model) — the one missing piece is exactly that Physlib TODO, isolated here as the single admission 47.
Throughout, \(K\) is a field (specialized to \(\mathbb C\) for the physical instantiations), and modules are finite-dimensional unless stated otherwise.