Dependencies

The \(\mathfrak {so}_4\) axioms: ordinary angular momentum \(J_x,J_y,J_z\) (Definition 18) plus a rescaled Runge–Lenz vector \(A_x,A_y,A_z\), given as data — no concrete Physlib-backed instance at fixed \(d=3\) yet.

\(\vec I := \tfrac 12(\vec J+\vec A)\), \(\vec K := \tfrac 12(\vec J-\vec A)\).

A vector \(\Omega \) annihilated by every \(a_i\); vacuumSpan L \(\Omega \) n is the span of all degree-\(n\) words \(a_{i_1}^\dagger \cdots a_{i_n}^\dagger \Omega \).

A Fin d-indexed family of creation/annihilation operator pairs \(a_i, a_i^\dagger \) on \(V\), satisfying the canonical commutation relations. The \(\mathfrak {gl}(d)\) analogue of Systems/Orthogonal/’s SoSystem (Definition 21).

The concrete data a special system must produce before invoking highest-weight theory: a nonzero vector, a Cartan weight for it, membership in the corresponding weight space, annihilation by every simple positive-root generator, and cyclic generation of the whole module. cyclic replaces any application-specific irreducibility assumption.

A \(Q\)-labeled decomposition of \(V\): \(V \cong \bigoplus _q \mathrm{sector}(q)\), internally (a thin name for DirectSum.IsInternal).

A finer scheme \(E\) (labeled by \(R\)) refines a coarser scheme \(D\) (labeled by \(Q\)) along \(f : R \to Q\) when every fine sector sits inside the coarse sector its label maps to, and each coarse sector is the join of the fine sectors mapping to it — the fact behind every nested quantum-number chain (\(n \to \ell \to m\) and its analogues).

\(E_{ii}\) restricted to \(\mathrm{vacuumSpan}(L,\Omega ,n)\) — playing the same role SoSystem.cartanGen (Theorem 22) plays for \(\mathfrak {so}(n{+}1)\).

\(H := \hbar \omega (N + d/2)\), for any LadderSystem (generic Fock content, not specific to the physical oscillator despite living in the HarmonicOscillator/ folder).

physlibA/physlibAc packaged as a genuine LadderSystem (Definition 10) on \(\mathcal S(\mathbb R^d,\mathbb C)\).

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\).

Given \(d{\gt}0\) modes and nonzero coupling, the excitation-number sectors assemble into a genuine Foundations.SpectralSector of the algebraic Hamiltonian.

Physlib’s angular-momentum operators on Schwartz space \(\mathcal S(\mathbb R^d,\mathbb C)\).

Ordinary angular momentum \(L\) together with a generalized Runge–Lenz vector \(A\), satisfying the \(\mathfrak {so}(n)\)/vector-transform/self-closure relations that promote \(\mathrm{Fin}(n{+}1)\to \mathrm{Fin}(n{+}1)\to \mathrm{End}_K(V)\) into a genuine SoSystem.

A Fin M-indexed antisymmetric generator family \(\mathrm{gen} : \mathrm{Fin}\, M \to \mathrm{Fin}\, M \to \mathrm{End}_K(V)\) satisfying the \(\mathfrak {so}(M)\) structure constants — gives a genuine \(\mathfrak {so}(M)\)-module structure on \(V\) for free. The orthogonal analogue of Fock/’s LadderSystem (Definition 10).

Three operators \(J_x,J_y,J_z\) on a state space \(V\) satisfying the \(\mathfrak {so}_3\) commutation relations \([J_x,J_y]=iJ_z\) and cyclic permutations, given as abstract data (not derived from a concrete Hilbert-space realization at this layer).

A triple \((h,e,f)\) with \(h\neq 0\), \([e,f]=h\), \([h,e]=2e\), \([h,f]=-2f\) — already in Mathlib, with the whole primitive-vector string calculus, the classification of finite-dimensional irreducible \(\mathfrak {sl}_2\)-modules (one per dimension), and triangularizability over an algebraically closed field.

Theorem 20 applied to IRep.isSl2Triple/KRep.isSl2Triple, fed Theorem 63 directly. Not itself consumed further: the capstone (Theorem 69) goes through Theorem 65 instead — real, correct, and genuinely disconnected from the rest of this section; see SORRIES.md.

\([I_x,I_y]=iI_z\) and cyclic permutations; likewise for \(K\).

Immediate from Theorem 65: \(\dim V = n^2\) for some positive \(n\).

Unconditional, given Theorems 65 and 68: \(E = -\frac{mk^2}{2\hbar ^2n^2}\) for a positive integer \(n\), and \(\dim V = n^2\) — the classical Pauli derivation of hydrogen’s \(n^2\)-fold degeneracy, from group theory alone.

General conditional algebra, kept unchanged: unconditionally true given any matching Casimir data for \(I\) and \(K\), not itself a stand-in for something unproven.

\(\dim V = (p+1)^2\) for some \(p\in \mathbb N\) — i.e. the two \(\mathfrak {sl}_2\)-labels from Theorem 64 are secretly equal (\(m=n\)), which is what actually gives the \(n^2\) (not merely \((m+1)(n+1)\)) degeneracy. The concrete consequence Theorem 62 would give if fed the real bound state’s explicit Casimir-eigenvalue data — which needs isotypic-decomposition machinery (Sl2/Isotypic.lean stays archived, its own three sorrys unresolved) this project doesn’t have yet. Stated directly rather than mis-derived.

\([I_a,K_b]=0\) for all \(a,b\in \{ x,y,z\} \) — the two copies of \(\mathfrak {so}_3\) genuinely decouple.

The physical bound-state eigenspace is irreducible under the joint action of \(I\) and \(K\) together (all six generators) — genuinely weaker than either factor’s own irreducibility. The naive alternative — deriving this from \(I\) alone being irreducible — is mathematically wrong, not merely harder: if \(V \cong V(m)\otimes V(n)\) with \(n{\gt}0\) (every excited state), \(I\) acting alone on \(V\) decomposes into \(n+1\) copies of \(V(m)\), not irreducible. See Hydrogen/Exceptional/Spectrum.lean’s docstring for the full argument.

Genuinely general: expressing the Hamiltonian in terms of \(J^2+A^2\) and the shared Casimir eigenvalue yields this relation, and solving for \(E\) is honest algebra — not a physics-content hypothesis in disguise.

\(H.m\cdot H.k^2 = -2\cdot H.E\cdot \hbar ^2\cdot (p+1)^2\) for the physical \(H\) and the principal quantum number Theorem 65 gives. Standard textbook input (cf. Physlib’s hamiltonianRegCLM/lrlOperatorSqr_eq), not yet connected to a concrete eigenstate — the same gap Theorem 47 names for the general-dimension story, reappearing here.

Any symmetric ladder system (creation/annihilation mutually adjoint w.r.t. some anisotropic pairing — the algebraic surrogate for “position and momentum are self-adjoint”) has a genuine vacuum, and every fixed-excitation-number state is vacuum-generated: the textbook fact that makes “Fock space” and “the CCR representation” synonymous. A real proof would complete \(V\) to an actual Hilbert space and invoke the spectral theorem for the resulting self-adjoint number operator — genuine, standard analysis, admitted here at exactly the generality any CCR representation needs.

\(\dim \mathrm{vacuumSpan}(L,\Omega ,n) = \binom {d+n-1}{n}\).

\(E_{ij} := a_i^\dagger a_j\) satisfy \([E_{ij}, E_{kl}] = \delta _{jk}E_{il} - \delta _{li}E_{kj}\), giving \(V\) a genuine \(\mathfrak {gl}(d)\)-module structure.

The occupation-number states, indexed by degree-\(n\) count functions CountFun d n, form a genuine Basis of the degree-\(n\) vacuum-generated sector — via eigenvectors at pairwise-distinct eigenvalues of one diagonal operator, not assumed.

The degree-\(n\) vacuum-generated sector is linearly isomorphic to the free \(K\)-module on \(\mathrm{Sym}(\mathrm{Fin}\ d,\, n)\), the standard combinatorial model of \(\mathrm{Sym}^n(K^d)\).

Every finite-dimensional module’s character is a nonnegative integral combination of irreducible Weyl characters — full complete reducibility, beyond the single-irrep case of Theorem 6. Not yet consumed by either physical system: both currently work with a single eigenspace known or admitted to already be one irrep, so neither needs the multi-irrep decomposition yet.

The irreducibility half of Theorem 6, extracted. This is the theorem Hydrogen/Classification.lean calls, literally, and the theorem HarmonicOscillator/WeylClassification.lean’s docstring names as its intended target — see Theorem 49 and the remark at Theorem 31.

A finite, pairwise-commuting family of semisimple operators’ simultaneous eigenspaces form a quantum-number scheme. Independence and generalized-eigenspace spanning are both free for a commuting family; semisimplicity is used only to collapse generalized eigenspaces to ordinary ones. This is the theorem §3.4 and §4.5 both call, literally, on their own respective Cartan families — see Theorem 37 and Theorem 52.

A two-step refinement chain \(D \leftarrow E \leftarrow F\) is itself a one-step refinement along the composed label map.

Over an algebraically closed field of characteristic zero, a finite-dimensional cyclic highest-weight module for a semisimple Lie algebra is the irreducible module of that dominant highest weight, and its formal character is the Weyl character. Packages complete reducibility, the classification of finite-dimensional simple modules by dominant integral highest weights, and the Weyl character formula, all at once — deliberately not specialized to any one physical system.

For a based root datum and Weyl vector, a family of Weyl characters exists, satisfying the cross-multiplied Weyl formula, unique, linearly independent, with the division-free dimension formula. The Weyl denominator theorem / Demazure-operator argument from general Lie theory, deliberately never attempted here. Not yet consumed by either physical system — see SORRIES.md.

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.

\([a_i,a_j^\dagger ] = \delta _{ij}\), proved from Physlib’s underlying \([\mathbf x,\mathbf p]\) relation, not assumed.

With \(\hbar \omega \neq 0\) and Fock-completeness, \(\mathrm{eigenspace}(H,\hbar \omega (n+d/2)) = \mathrm{vacuumSpan}(L,\Omega ,n)\).

\(\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.

Standard real-analysis (positivity of \(\int |f|^2\) over a nonempty open set), not built elsewhere in this project.

physlibSpectralSector: Definition 32 applied concretely to physlibLadderSystem, with a vacuum chosen via Theorem 28.

\(\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.

HarmonicOscillator/Summary.lean item 9.

HarmonicOscillator/Summary.lean item 14, cited a second time from Hydrogen/Summary.lean — see Theorem 57.

HarmonicOscillator/Summary.lean item 4: a direct citation, zero new proof content.

Free, from Theorem 13 applied to physlibLadderSystem, given Theorems 26–27.

\(\mathrm{vacuumSpan}(L,\Omega ,n)\) decomposes into simultaneous cartanFamily-eigenspaces, via Theorem 4 applied directly — the same Foundations theorem Theorem 52 calls for \(\mathfrak {so}(n{+}1)\).

Closes a gap Physlib itself leaves @[sorryful]: proved independently here, reusing only Physlib’s own already-proved companion commutators.

Standard once \(\mathfrak {so}(n{+}1)\)’s Weyl/root-datum machinery exists, not otherwise attacked here. Mirrors Theorem 36 exactly.

The literal shared-with-the-oscillator invocation: a direct specialization of Theorem 7 to HydrogenSoData’s \(\mathfrak {so}(n{+}1)\)-module — no new representation theory, only type-matching. Not yet fed the concrete root-datum/highest-weight-vector data (needs genuine spectral theory, per Theorem 47), so nothing downstream invokes it at a concrete instance yet.

At a fixed (implicit) principal quantum number \(N\): \(V\) is irreducible under the full hidden symmetry (Theorem 50) and splits into simultaneous eigenspaces of the concrete Cartan subalgebra, the magnetic numbers (Theorem 52).

For hydrogen there is no bigger dynamical group to descend from (unlike the oscillator’s \(\mathfrak {gl}(d)\), strictly bigger than the physical rotation group), so the entire level-\(N\) bound-state eigenspace being one \(\mathfrak {so}(n{+}1)\)-irrep is this fact. Blocked on the same missing type-\(B_r/D_r\) root-datum gap as Theorem 49.

\([A(\varepsilon )_i,A(\varepsilon )_j]\)’s operator-valued coefficient (from Physlib’s lrl_commutation_lrl) collapses to the plain scalar \(-i/\hbar \) — true exactly on a genuine bound-state energy eigenspace, where the Hamiltonian and \(\mathbf r(\varepsilon )^{-3}\) each act by their eigenvalue/expectation value. The entire missing hydrogen spectral-theory front, converted into one precise, directly-admitted statement: Physlib itself lists the hydrogen point spectrum as an unstarted TODO.

Builds a HydrogenSoData from any operator family satisfying the angular-momentum relations and a scalar Runge–Lenz self-commutator hypothesis — the general constructor Theorem 48 specializes.

physlibGen genuinely satisfies SoSystem’s exact structure constants.

Unconditional, given Theorem 47: zero further sorry.

HydrogenSoData packages exactly the data SoSystem (Definition 21) needs.

Hydrogen/Summary.lean item 5 — the same Foundations theorem the oscillator’s WeylClassification.lean targets, \(\mathfrak {so}(n{+}1)\) in place of \(\mathfrak {gl}(d)\).

Hydrogen/Summary.lean item 8, the closing citation of the whole joint blueprint.

Hydrogen/Summary.lean item 6.

Hydrogen/Summary.lean item 7: this leaf reaches directly into HarmonicOscillator/QuantumNumbers.lean, citing Theorem 37 from the other physical system’s file — concrete, checkable evidence the sharing claimed throughout this blueprint is real, not aspirational.

Hydrogen/Summary.lean item 4.

\(V\) decomposes into simultaneous cartanGen-eigenspaces, via Theorem 4 applied directly to \(\mathfrak {so}(n{+}1)\)’s Cartan family — the same Foundations theorem Theorem 37 calls for \(\mathfrak {gl}(d)\).

A canonical, pairwise-commuting family \(\mathrm{cartanGen} : \mathrm{Fin}\lfloor M/2\rfloor \to \mathrm{End}_K(V)\), built by pairing up generators two at a time — the concrete Cartan subalgebra any SoSystem carries for free.

If \(J_z\neq 0\), then \((2J_z,\, J_x+iJ_y,\, J_x-iJ_y)\) is an \(\mathfrak {sl}_2\)-triple.

Two \(\mathfrak {sl}_2\)-triples on a finite-dimensional \(V\) over an algebraically closed characteristic-zero field, commuting with each other, with no proper subspace invariant under both actions jointly, force \(\dim _K V = (m+1)(n+1)\) for some \(m,n\in \mathbb N\). Proved via a joint primitive vector (Systems/Sl2/BivariateBasis.lean): commutativity lets a highest-weight vector for the first triple be found inside a weight space invariant under the second, giving one vector primitive for both, whose bivariate string is a basis. This is the engine Hydrogen/Exceptional/Spectrum.lean uses to turn the \(\mathfrak {so}_4\cong \mathfrak {so}_3\oplus \mathfrak {so}_3\) decoupling into a dimension count — see Theorem 64.