Angular momentum coupling, the Wigner–Eckart theorem and the hydrogen spectrum, formally verified in Lean 4

We describe a formalisation in Lean 4 and Mathlib, merged into physlib, of angular momentum coupling and of the non-relativistic hydrogen spectrum. Clebsch–Gordan coefficients are defined as values of a contravariant bilinear form on normalised lowering strings of explicit highest-weight vectors of sl2-modules over the reals; tensor products are decomposed without a complete reducibility theorem. We prove both orthogonality relations, the Condon–Shortley phase, a closed formula and Racah's formula, the latter by showing that two alternating binomial sums satisfy the same recursion. The 3j symbol is shown to be invariant up to sign under the row and column permutations and the transposition of its Regge square; recoupling coefficients of three angular momenta are independent of M and have orthonormal columns; the 6j symbol defined by recoupling equals, for non-zero outer spins, the sum over four 3j symbols, and this sum is invariant under all 24 vertex permutations of its tetrahedron. The Wigner–Eckart theorem is proved for sl2 standard modules, for irreducible angular momentum representations of non-zero spin, and in Clebsch–Gordan form, with the projection theorem, selection rules and a multipole sum rule. For hydrogen we prove the radial equation and expectation values for the Laguerre radial functions; quantisation E = −1/ν², without a power-series ansatz, for non-zero square-integrable solutions with E < 0 that vanish at the origin; bound states in d dimensions; Pauli's algebraic derivation for abstract operators; L·A = 0 for the regularised Laplace–Runge–Lenz operator; and the first-order fine-structure formula. All statements carry their Lean names at a fixed commit; physical input is listed explicitly. Rational 3j and 6j values checked in the Lean kernel (not yet merged) and an application to selection rules in ENSDF are reported.