1 Foundations: the shared backend
Everything in this chapter is either fully proved for real, at full generality, or is one of the handful of deliberate admissions this project makes at the general semisimple-Lie-algebra level — never re-admitted per physical system. Both HarmonicOscillator/ and Hydrogen/ literally call into this chapter’s theorems; that is the concrete evidence, checked by the graph below rather than asserted in prose, that this project has genuinely shared machinery and not merely two parallel developments.
1.1 Labeled decompositions
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).
A two-step refinement chain \(D \leftarrow E \leftarrow F\) is itself a one-step refinement along the composed label map.
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.
1.2 The highest-weight / Weyl boundary
This is the one place in the project where an admission is deliberate at full generality: a finite-dimensional cyclic highest-weight module for a semisimple Lie algebra, over an algebraically closed characteristic-zero field, is irreducible with the expected Weyl character. Concrete systems never re-derive this; they exhibit a cyclic highest-weight vector and inherit the conclusion.
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.
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.
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.