TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite spin-block decomposition

Statement

Let $V$ be a nonzero finite-dimensional complex inner product space, with inner product linear in the first argument (Real and complex inner product spaces, with the inner product linear in the first argument, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis), and let $J_{x}, J_{y}, J_{z} \in End (V)$ be self-adjoint operators satisfying (Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space)

$[J_{x}, J_{y}] = i J_{z}, [J_{y}, J_{z}] = i J_{x}, [J_{z}, J_{x}] = i J_{y} .$

Put $J_{+} : = J_{x} + i J_{y}$ , $J_{-} : = J_{x} - i J_{y}$ and $J^{2} : = J_{x}^{2} + J_{y}^{2} + J_{z}^{2}$ . Then:

(a) $J_{+}^{*} = J_{-}$ , $J_{-}^{*} = J_{+}$ , $[J_{z}, J_{\pm}] = \pm J_{\pm}$ , $[J_{+}, J_{-}] = 2 J_{z}$ , $J^{2} = J_{-} J_{+} + J_{z}^{2} + J_{z} = J_{+} J_{-} + J_{z}^{2} - J_{z}$ , and $J^{2}$ is self-adjoint, commutes with $J_{x}, J_{y}, J_{z}, J_{\pm}$ , and satisfies $⟨ J^{2} v, v ⟩ = ∥ J_{x} v ∥^{2} + ∥ J_{y} v ∥^{2} + ∥ J_{z} v ∥^{2} \geq 0$ for every $v \in V$ ;

(b) there are an integer $r \geq 1$ , numbers $j_{1}, \dots, j_{r} \in \frac{1}{2} N = {0, \frac{1}{2}, 1, \dots}$ with $\sum_{ν = 1}^{r} (2 j_{ν} + 1) = \dim V$ , and an orthonormal basis $(v_{ν, k})$ , $ν \in {1, \dots, r}$ , $k \in {0, 1, \dots, 2 j_{ν}}$ , of $V$ such that

$J_{z} v_{ν, k} = (j_{ν} - k) v_{ν, k}, J_{+} v_{ν, k} = \sqrt{k (2 j_{ν} - k + 1)} v_{ν, k - 1}, J_{-} v_{ν, k} = \sqrt{(k + 1) (2 j_{ν} - k)} v_{ν, k + 1},$

$J^{2} v_{ν, k} = j_{ν} (j_{ν} + 1) v_{ν, k}, J_{x} v_{ν, k} = \frac{1}{2} (J_{+} + J_{-}) v_{ν, k}, J_{y} v_{ν, k} = \frac{1}{2 i} (J_{+} - J_{-}) v_{ν, k},$

with $v_{ν, - 1} : = 0$ and $v_{ν, 2 j_{ν} + 1} : = 0$ ; each summand $V_{ν} : = span {v_{ν, 0}, \dots, v_{ν, 2 j_{ν}}}$ is $J_{x}, J_{y}, J_{z}$ -invariant, the decomposition $V = ⨁_{ν = 1}^{r} V_{ν}$ is orthogonal, and the map $v_{ν, k} \mapsto e_{j_{ν} - k}$ is a unitary equivalence of $(J_{x}, J_{y}, J_{z})$ on $V_{ν}$ with the spin- $j_{ν}$ matrices of Finite spin matrices;

(c) let $λ$ be the largest eigenvalue of $J_{z}$ (it exists and is real), and let $u \neq 0$ satisfy $J_{z} u = λ u$ . Then $λ \geq 0$ , $J_{+} u = 0$ , and with $w_{k} : = J_{-}^{k} u$ one has $w_{k} \neq 0$ for $0 \leq k \leq 2 λ$ , $w_{k} = 0$ for $k = 2 λ + 1$ , $2 λ \in N$ , and $∥ w_{k} ∥^{2} = k! (2 λ) (2 λ - 1) \dots (2 λ - k + 1) ∥ u ∥^{2}$ for $0 \leq k \leq 2 λ + 1$ ; the vectors $w_{k} / ∥ w_{k} ∥$ , $0 \leq k \leq 2 λ$ , form the block of (b) with $j = λ$ ; consequently $λ \in \frac{1}{2} N$ and the largest eigenvalue of $J_{z}$ on each block is one of the numbers $j_{1}, \dots, j_{r}$ ;

(d) for every $M \in \frac{1}{2} N$ the number of blocks with $j_{ν} \in M + Z$ and $j_{ν} \geq M$ equals $\dim \ker (J_{z} - M I)$ , and the number of blocks with $j_{ν} = M$ equals $\dim \ker (J_{z} - M I) - \dim \ker (J_{z} - (M + 1) I)$ ; in particular the multiset ${j_{1}, \dots, j_{r}}$ is determined by the pair $(V, J_{z})$ together with the relations, and the spectrum of $J_{z}$ is the multiset union of the numbers $j_{ν} - k$ , $0 \leq k \leq 2 j_{ν}$ (a block with parameter $j$ contributes its weights only to the lattice coset $j + Z$ ).

No physical interpretation of the operators as angular momentum, spin or observables is asserted; the theorem is a classification of finite-dimensional triples satisfying the displayed commutation relations.

Facts & Assumptions

Given: a nonzero finite-dimensional complex inner product space $V$ ; self-adjoint $J_{x}, J_{y}, J_{z}$ satisfying the three commutation relations; the derived operators $J_{\pm}$ and $J^{2}$ .

[F1]

Adjoints are conjugate-linear, $(T^{*})^{*} = T$ , $(T + T^{'})^{*} = T^{*} + T^{'}$ , $(T T^{'})^{*} = T^{' *} T^{*}$ , and a restriction of a self-adjoint operator to a closed invariant subspace is self-adjoint; self-adjoint operators are normal (The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ , Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space).

[F2]

Every self-adjoint endomorphism of a nonzero finite-dimensional complex inner product space has a real eigenvalue and a unit eigenvector, so its set of eigenvalues is a nonempty finite subset of $R$ and has a largest element (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F3]

For a self-adjoint $T$ and eigenvectors $u, v$ with $T u = λ u$ , $T v = μ v$ and $λ \neq μ$ one has $⟨ u, v ⟩ = 0$ : $(λ - μ) ⟨ u, v ⟩ = ⟨ T u, v ⟩ - ⟨ u, T v ⟩ = 0$ ; the orthogonal complement of an invariant subspace is invariant for a self-adjoint operator; and $⟨ T^{2} v, v ⟩ = ∥ T v ∥^{2}$ for self-adjoint $T$ (Orthogonality and the orthogonal complement, Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space, Real and complex inner product spaces, with the inner product linear in the first argument).

[F4]

The norm satisfies $∥ v ∥^{2} = ⟨ v, v ⟩ \geq 0$ , $∥ v ∥ = 0$ iff $v = 0$ , and $⟨ T v, w ⟩ = ⟨ v, T^{*} w ⟩$ for all $v, w$ (The induced length is a norm, The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ ).

[F5]

An orthogonal decomposition $V = W \oplus W^{⊥}$ has $\dim V = \dim W + \dim W^{⊥}$ , and a finite orthogonal family of nonzero vectors is linearly independent (Orthogonality and the orthogonal complement, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, Linear subspace of a vector space).

[F6]

The matrices of Finite spin matrices for $s = j$ act on an orthonormal basis $e_{m}$ , $- j \leq m \leq j$ , by the formulas displayed in the Statement with $s = j$ , are self-adjoint, satisfy the same commutation relations, and have $J^{2} = j (j + 1) I$ (Finite spin matrices).

[F7]

For integers $0 \leq k \leq m$ the products $k! (2 λ) (2 λ - 1) \dots (2 λ - k + 1)$ vanish if and only if $2 λ$ is a nonnegative integer strictly less than $k$ ; sums of dimensions over a finite orthogonal direct sum add (The natural numbers $N$ (von Neumann), A finite sum in a commutative monoid indexed by an arbitrary finite set, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis).

Proof

1.1F1F3F4algebra

[The derived algebra] Taking adjoints of $J_{\pm} = J_{x} \pm i J_{y}$ with $J_{x}^{*} = J_{x}$ , $J_{y}^{*} = J_{y}$ and the conjugation laws gives $J_{+}^{*} = J_{-}$ and $J_{-}^{*} = J_{+}$ . The commutation relations give $[J_{z}, J_{\pm}] = [J_{z}, J_{x}] \pm i [J_{z}, J_{y}] = i J_{y} \pm i (- i J_{x}) = \pm (J_{x} \pm i J_{y}) = \pm J_{\pm}$ and $[J_{+}, J_{-}] = [J_{x} + i J_{y}, J_{x} - i J_{y}] = - i [J_{x}, J_{y}] + i [J_{y}, J_{x}] = 2 J_{z}$ . Direct expansion gives $J_{-} J_{+} = J_{x}^{2} + J_{y}^{2} - J_{z} = J^{2} - J_{z}^{2} - J_{z}$ and $J_{+} J_{-} = J_{x}^{2} + J_{y}^{2} + J_{z} = J^{2} - J_{z}^{2} + J_{z}$ , hence $J^{2} = J_{-} J_{+} + J_{z}^{2} + J_{z} = J_{+} J_{-} + J_{z}^{2} - J_{z}$ . Since $J_{\pm}$ and $J^{2}$ are polynomials in the self-adjoint $J_{i}$ , [F1] gives $J^{2 *} = J^{2}$ . Finally $[J^{2}, J_{x}] = [J_{y}^{2}, J_{x}] + [J_{z}^{2}, J_{x}] = J_{y} [J_{y}, J_{x}] + [J_{y}, J_{x}] J_{y} + J_{z} [J_{z}, J_{x}] + [J_{z}, J_{x}] J_{z} = - i (J_{y} J_{z} + J_{z} J_{y}) + i (J_{z} J_{y} + J_{y} J_{z}) = 0$ , and cyclically $[J^{2}, J_{y}] = [J^{2}, J_{z}] = 0$ , so $J^{2}$ commutes with $J_{x}, J_{y}, J_{z}$ and hence with $J_{\pm}$ ; and $⟨ J^{2} v, v ⟩ = ⟨ J_{x}^{2} v, v ⟩ + ⟨ J_{y}^{2} v, v ⟩ + ⟨ J_{z}^{2} v, v ⟩ = ∥ J_{x} v ∥^{2} + ∥ J_{y} v ∥^{2} + ∥ J_{z} v ∥^{2} \geq 0$ by [F3], [F4]. This proves (a).

2.1step 1.1F2F3F4algebra

[A highest vector] By [F2] $J_{z}$ has a largest eigenvalue $λ \in R$ and a unit eigenvector $u$ with $J_{z} u = λ u$ , where $u \neq 0$ because $∥ u ∥ = 1$ . From $[J_{z}, J_{+}] = J_{+}$ of step 1.1, $J_{z} (J_{+} u) = J_{+} J_{z} u + J_{+} u = (λ + 1) J_{+} u$ , so $J_{+} u$ is either $0$ or an eigenvector of $J_{z}$ with eigenvalue $λ + 1$ ; maximality of $λ$ forces $J_{+} u = 0$ . Applying step 1.1 to $u$ gives $⟨ J^{2} u, u ⟩ = ⟨ (J_{+} J_{-} + J_{z}^{2} - J_{z}) u, u ⟩ = ⟨ J_{+} J_{-} u, u ⟩ + λ^{2} - λ$ , while $⟨ J^{2} u, u ⟩ \geq λ^{2}$ by (a); equivalently, since $J_{+} u = 0$ , $J_{+} J_{-} u = J_{+} J_{-} u - J_{-} J_{+} u = [J_{+}, J_{-}] u = 2 J_{z} u = 2 λ u$ and therefore $⟨ J^{2} u, u ⟩ = 2 λ + λ^{2} - λ = λ (λ + 1) \geq ∥ J_{z} u ∥^{2} = λ^{2}$ , so $λ \geq 0$ .

3.1step 1.1step 2.1F3F4F5algebra

[The string and its length] Define $w_{k} : = J_{-}^{k} u$ for $k \in N$ , so $w_{0} = u$ . Inductively, $J_{z} w_{k} = (J_{-} J_{z} - J_{-}) J_{-}^{k - 1} u = (λ - k) w_{k}$ by step 1.1, and using $J_{+} J_{-} = J^{2} - J_{z}^{2} + J_{z}$ , the fact that $J^{2}$ commutes with $J_{-}$ and $J^{2} u = λ (λ + 1) u$ from step 2.1, one computes $J_{+} w_{k} = J_{+} J_{-} w_{k - 1} = (J^{2} - J_{z}^{2} + J_{z}) w_{k - 1} = [λ (λ + 1) - (λ - k + 1)^{2} + (λ - k + 1)] w_{k - 1} = k (2 λ - k + 1) w_{k - 1}$ for $k \geq 1$ . Pairing with $w_{k - 1}$ and using [F4] gives the recursion $∥ w_{k} ∥^{2} = k (2 λ - k + 1) ∥ w_{k - 1} ∥^{2}$ , hence $∥ w_{k} ∥^{2} = k! (2 λ) (2 λ - 1) \dots (2 λ - k + 1) ∥ u ∥^{2}$ by induction, the case $k = 0$ being the empty product. If $w_{k} \neq 0$ for every $k$ , the vectors $w_{k}$ are nonzero eigenvectors of $J_{z}$ for the pairwise distinct eigenvalues $λ, λ - 1, λ - 2, \dots$ ; any $\dim V + 1$ of them form an orthogonal family of nonzero vectors, hence are linearly independent by [F3] and [F5], which is impossible in the finite-dimensional space $V$ . So there is a least $m \geq 1$ with $w_{m} = 0$ , and then $0 = ∥ w_{m} ∥^{2} = m (2 λ - m + 1) ∥ w_{m - 1} ∥^{2}$ forces $2 λ = m - 1 \in N$ .

4.1step 1.1step 2.1step 3.1F3F6algebra

[The normalized block] Put $2 j : = m - 1 = 2 λ$ with $j = λ \in \frac{1}{2} N$ , and for $0 \leq k \leq 2 j$ set $v_{k} : = w_{k} / ∥ w_{k} ∥$ , which is defined because $w_{k} \neq 0$ for $k < m = 2 j + 1$ and unit by construction. The eigenvectors $w_{k}$ have distinct eigenvalues $j, j - 1, \dots, - j$ of the self-adjoint $J_{z}$ , so they are pairwise orthogonal by [F3]; hence $v_{0}, \dots, v_{2 j}$ is an orthonormal family. The action formulas follow from steps 1.1, 2.1 and 3.1: $J_{z} v_{k} = (j - k) v_{k}$ ; $J_{-} v_{k} = ∥ w_{k + 1} ∥ / ∥ w_{k} ∥ v_{k + 1} = \sqrt{(k + 1) (2 j - k)} v_{k + 1}$ for $k < 2 j$ and $J_{-} v_{2 j} = 0$ ; $J_{+} v_{k} = k (2 j - k + 1) ∥ w_{k - 1} ∥ / ∥ w_{k} ∥ v_{k - 1} = \sqrt{k (2 j - k + 1)} v_{k - 1}$ for $k \geq 1$ and $J_{+} v_{0} = 0$ ; and $J^{2} v_{k} = λ (λ + 1) v_{k} = j (j + 1) v_{k}$ because $J^{2}$ commutes with $J_{-}$ . The span $V_{λ} : = span {v_{0}, \dots, v_{2 j}}$ is therefore invariant under $J_{\pm}$ and $J_{z}$ , hence under $J_{x}, J_{y}, J_{z}$ , and [F6] identifies the action with the spin- $j$ model, giving $J_{x} v_{k} = \frac{1}{2} (J_{+} + J_{-}) v_{k}$ and $J_{y} v_{k} = \frac{1}{2 i} (J_{+} - J_{-}) v_{k}$ .

5.1step 4.1F1F3F5algebra

[The invariant complement] Let $W : = V_{λ}$ . If $w \in W^{⊥}$ and $w^{'} \in W$ , then for each $i$ the invariance of $W$ and self-adjointness of $J_{i}$ give $⟨ J_{i} w, w^{'} ⟩ = ⟨ w, J_{i} w^{'} ⟩ = 0$ , so $J_{i} w \in W^{⊥}$ ; thus $W^{⊥}$ is invariant under $J_{x}, J_{y}, J_{z}$ . The restriction of each $J_{i}$ to $W^{⊥}$ is self-adjoint by [F1], the commutation relations hold there, and $V = W \oplus W^{⊥}$ is an orthogonal direct sum with $\dim V = \dim W + \dim W^{⊥}$ by [F5]; if $W^{⊥} \neq {0}$ , the restricted triple again satisfies the hypotheses of the Statement.

6.1step 2.1step 3.1step 4.1step 5.1F5F6F7algebra

[Exhaustion and the decomposition] Iterate step 5.1: as long as the orthogonal complement of the blocks already produced is nonzero, step 2.1 supplies a largest eigenvalue and step 4.1 a further nonzero invariant block of dimension $2 j_{ν} + 1 \geq 1$ , orthogonally split off, decreasing the dimension of the complement by $2 j_{ν} + 1$ . Since the dimension is a nonnegative integer, the process terminates after some finite number $r \geq 1$ of blocks with complement ${0}$ , yielding an orthogonal decomposition $V = ⨁_{ν = 1}^{r} V_{ν}$ and an orthonormal basis $(v_{ν, k})$ as in (b); the basis is orthonormal as a union of the block bases because the blocks are pairwise orthogonal, and $\sum_{ν} (2 j_{ν} + 1) = \dim V$ by additivity of dimensions in orthogonal direct sums [F5], [F7]. Each block action is the spin- $j_{ν}$ action by step 4.1 and [F6], which proves (b); step 3.1 applied to a block identifies the largest eigenvalue of $J_{z}$ on that block as $j_{ν}$ , completing (c) except for $λ \geq 0$ , proved in step 2.1.

7.1step 6.1algebra∎

[Multiplicity count] Let $M \in \frac{1}{2} N$ and consider the eigenvalue- $M$ eigenspace of $J_{z}$ . A block with parameter $j$ contributes the basis vector with $k = j - M$ exactly when $j \in M + Z$ and $0 \leq M \leq j$ , and contributes nothing in all other cases (its weights are $j, j - 1, \dots, - j$ , all in the coset $j + Z$ ); hence $\dim \ker (J_{z} - M I) = # {ν : j_{ν} \in M + Z, j_{ν} \geq M}$ by the orthonormal basis of step 6.1. Applying this at $M$ and at $M + 1$ , both in the same coset $M + Z$ , and subtracting gives $# {ν : j_{ν} = M} = \dim \ker (J_{z} - M I) - \dim \ker (J_{z} - (M + 1) I)$ . The multiset ${j_{1}, \dots, j_{r}}$ is therefore determined by $J_{z}$ (using the fixed relations to know that the decomposition exists), and the spectrum statement follows by collecting the eigenvalues $j_{ν} - k$ of the blocks; the coset qualifier in (d) excludes nothing, since blocks outside $M + Z$ contribute no vector to either eigenspace. This proves (d).

Finite spin-block decomposition

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources