Solution (source code)

= Solution

For a local spin quantized along its positive $\tilde z$ axis, the exact <Holstein–Primakoff transformation> is
$$
\boxed{\tilde S_j^z=S-n_j,\quad
\tilde S_j^+=\sqrt{2S-n_j}\,a_j,\quad
\tilde S_j^-=a_j^\dagger\sqrt{2S-n_j},\quad n_j=a_j^\dagger a_j.}
$$
The bosonic operators obey $[a_j,a_k^\dagger]=\delta_{jk}$. The physical local subspace is $0\leq n_j\leq2S$; the larger unconstrained boson <Fock space> is not itself the finite spin Hilbert space. The ordering of the square roots matters, since $n_j$ does not commute with $a_j$.

This represents spin lowering using a bosonic <creation operator>, making a fully polarized spin state the boson vacuum. On the physical subspace it reproduces the spin <commutators> and the Casimir $\tilde{\mathbf S}_j^2=S(S+1)$. Expanding the square roots for small occupation relative to $S$ organizes a controlled large-$S$ <linear spin-wave approximation>; it is not an assumption that a spin has an infinite number of physical levels.