2 System structures
Physics-free machinery, each physical system instantiates one or more of these.
2.1 Bosonic CCR / Fock
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).
\(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.
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 \).
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.
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.
\(\dim \mathrm{vacuumSpan}(L,\Omega ,n) = \binom {d+n-1}{n}\).
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)\).
2.2 \(\mathfrak {sl}_2\), angular momentum, and commuting pairs
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.
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).
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.
2.3 The orthogonal engine
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).
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.