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

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

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

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.

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.

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

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

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.

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.

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