ExampleConstruction: AI-adaptedVerification: 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.

Orbital core commutators

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Use the notation of Orbital self-adjoint generators: $S^{2} = {x \in R^{3} : ∣ x ∣ = 1}$ with polar measure $σ$ , the Hilbert space $L^{2} (S^{2}, σ)$ with inner product linear in the first argument, the operators $L_{1}, L_{2}, L_{3}$ with $L_{\pm} : = L_{1} \pm i L_{2}$ , the finite span $H$ , the blocks $V_{l}$ , and the first-order operators $D_{i}$ , so that $L_{i} = - i ℏ D_{i}$ on $H$ . Let $d : = \sqrt{3 / (4 π)}$ and, writing $Ω = (Ω_{1}, Ω_{2}, Ω_{3})$ for the points of $S^{2}$ and restricting the coordinate polynomials, $v_{1} : = - \frac{d}{\sqrt{2}} (Ω_{1} + i Ω_{2}), v_{0} : = d Ω_{3}, v_{- 1} : = \frac{d}{\sqrt{2}} (Ω_{1} - i Ω_{2}) \in V_{1} .$ Then:

(a) $(v_{1}, v_{0}, v_{- 1})$ is an orthonormal basis of $V_{1}$ , and it is the degree-one part of the family $(Y_{l m})$ , in the sense that $v_{m} = Y_{1, m} (m \in {1, 0, - 1})$ as elements of $L^{2} (S^{2}, σ)$ (Associated Legendre function normalization);

(b) the core commutators hold on the whole three-dimensional space $V_{1}$ : $L_{3} v_{m} = ℏ m v_{m}, L_{+} v_{1} = 0, L_{+} v_{0} = \sqrt{2} ℏ v_{1}, L_{+} v_{- 1} = \sqrt{2} ℏ v_{0},$ with $(L_{-} ∣_{V_{1}}) = (L_{+} ∣_{V_{1}})^{*}$ (adjoint in the finite Hilbert space $V_{1}$ ) giving $L_{-} v_{- 1} = 0$ , $L_{-} v_{0} = \sqrt{2} ℏ v_{- 1}$ , $L_{-} v_{1} = \sqrt{2} ℏ v_{0}$ ; and $[L_{1}, L_{2}] v = i ℏ L_{3} v, (L_{1}^{2} + L_{2}^{2} + L_{3}^{2}) v = 2 ℏ^{2} v (v \in V_{1});$

(c) the assignment $e_{m} \mapsto v_{m}$ ( $m = - 1, 0, 1$ ) is a unitary isomorphism of the spin- $1$ model $(V_{1}^{s p i n}, J_{x}, J_{y}, J_{z})$ of Finite spin matrices onto $V_{1}$ carrying $J_{i}$ to $ℏ^{- 1} L_{i}$ for $i = x, y, z$ : the orbital degree- $1$ block is unitarily equivalent to the spin- $1$ block, and $L_{1}^{2} + L_{2}^{2} + L_{3}^{2}$ acts on $V_{1}$ as $ℏ^{2} A$ , where $A$ is the diagonal sphere Laplacian of Sphere Laplacian diagonal domain with $A ∣_{V_{1}} = 2 i d$ .

All claims are finite-dimensional matrix computations inside $V_{1}$ ; no physical interpretation of the operators as angular momentum of a particle is asserted.

Facts & Assumptions

Given: the operators $L_{1}, L_{2}, L_{3}, L_{\pm}$ of the generators theorem, the functions $Ω_{i}$ , the number $d = \sqrt{3 / (4 π)}$ , and the vectors $v_{m}$ .

[F1]

Generators theorem (Orbital self-adjoint generators (a),(b)): for $F \in V_{l}$ with representative $p_{F}$ one has $L_{i} F = {r e s}_{l} (- i ℏ D_{i} p_{F})$ with $D_{i} p = (x \times \nabla p)_{i}$ , so $L_{i}$ maps $V_{l}$ into itself and $L_{i} = - i ℏ D_{i}$ on $H$ ; $L_{1}, L_{2}, L_{3}$ are self-adjoint and $L_{i} L_{j} - L_{j} L_{i} = i ℏ \sum_{k} ε_{i j k} L_{k}$ on $H$ ; and the everywhere-defined finite restrictions $A_{i} : = L_{i} ∣_{V_{1}}$ are Hermitian. Hence $A_{\pm} : = A_{1} \pm i A_{2}$ satisfy $A_{-} = (A_{+})^{*}$ as operators on $V_{1}$ : for $f, g \in V_{1}$ , $⟨ A_{+} f, g ⟩ = ⟨ f, (A_{1} - i A_{2}) g ⟩$ , since the inner product is first-variable linear. This is solely a finite-block adjoint identity, with no assertion about the full unbounded sum adjoint.

[F2]

The $L^{2}$ inner products of the coordinate functions: integrating over $S^{2}$ in angle coordinates, $\int_{S^{2}} Ω_{1}^{2} d σ = \int_{0}^{π} \int_{0}^{2 π} \sin^{2} θ \cos^{2} φ \sin θ d φ d θ = π \cdot \frac{4}{3} = \frac{4 π}{3}$ and likewise for $Ω_{2}^{2}, Ω_{3}^{2}$ , while all mixed integrals vanish, since $\int_{0}^{2 π} \cos φ d φ = \int_{0}^{2 π} \sin φ d φ = \int_{0}^{2 π} \sin φ \cos φ d φ = 0$ and the $θ$ -integrals factor; hence $⟨ Ω_{i}, Ω_{j} ⟩ = \frac{4 π}{3} δ_{i j}$ (Sphere integrals in angle coordinates, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, The complex exponential by its power series).

[F3]

The degree-one harmonics: $Y_{1, 0} = b_{10} w_{10} (\cos θ) / \sqrt{2 π}$ with $P_{1} (t) = t$ and $w_{10} = P_{1}$ , $b_{10} = (\int_{- 1}^{1} t^{2} d t)^{- 1 / 2} = \sqrt{3 / 2}$ , so $Y_{1, 0} = \sqrt{3 / (4 π)} Ω_{3}$ ; and $Y_{1, 1} = b_{11} w_{11} (\cos θ) e^{i φ} / \sqrt{2 π}$ with $w_{11} = - (1 - t^{2})^{1 / 2}$ and $b_{11} = (\int_{- 1}^{1} (1 - t^{2}) d t)^{- 1 / 2} = \sqrt{3 / 4}$ , so $Y_{1, 1} = - \sqrt{3 / (8 π)} (Ω_{1} + i Ω_{2})$ ; moreover $Y_{1, - 1} = - Y_{1, 1}$ -conjugate: $Y_{1, - 1} = (- 1)^{1} \overline{Y_{1, 1}} = \sqrt{3 / (8 π)} (Ω_{1} - i Ω_{2})$ , using $Ω_{1} + i Ω_{2} = \sin θ e^{i φ}$ on $S^{2}$ (Associated Legendre function normalization (a),(c), The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , The derivatives of sine and cosine are cosine and minus sine, Sine and cosine defined by their real power series, The complex exponential by its power series).

[F4]

The space $V_{1}$ and the diagonal operator: $V_{1}$ consists of the classes of the restrictions of the linear polynomials $Ω_{i}$ , the restriction map on harmonic homogeneous polynomials of degree $1$ is a linear isomorphism onto $V_{1}$ , and $A Y_{1, m} = 2 Y_{1, m}$ , so $A ∣_{V_{1}} = 2 i d$ (Harmonic polynomial dimension (b),(c), Sphere Laplacian diagonal domain (a), The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F5]

Spin-one data (Finite spin matrices): in the basis $(e_{m})_{m = 1, 0, - 1}$ one has $J_{z} e_{m} = m e_{m}$ , $J_{+} e_{1} = 0$ , $J_{+} e_{0} = \sqrt{2} e_{1}$ , $J_{+} e_{- 1} = \sqrt{2} e_{0}$ , $J_{-} = (J_{+})^{*}$ , and $J_{x} = \frac{1}{2} (J_{+} + J_{-})$ , $J_{y} = \frac{1}{2 i} (J_{+} - J_{-})$ ; the arrows $e_{m} \mapsto v_{m}$ with orthonormal domain and target bases are unitary ([F2], Real and complex inner product spaces, with the inner product linear in the first argument, The induced length is a norm).

Verification

1.1F2F3F4algebra

[(a) orthonormality and identification] By [F2], $∥ v_{0} ∥^{2} = d^{2} \frac{4 π}{3} = 1$ , $∥ v_{\pm 1} ∥^{2} = \frac{d^{2}}{2} (\frac{4 π}{3} + \frac{4 π}{3}) = 1$ , and $⟨ v_{1}, v_{0} ⟩ = ⟨ v_{1}, v_{- 1} ⟩ = ⟨ v_{0}, v_{- 1} ⟩ = 0$ ; so the $v_{m}$ are orthonormal, and since $\dim V_{1} = 3$ they form an orthonormal basis of $V_{1}$ ([F4]). Comparing with the displayed values of [F3]: $Y_{1, 0} = d Ω_{3} = v_{0}$ , $Y_{1, 1} = - \sqrt{3 / (8 π)} (Ω_{1} + i Ω_{2}) = - \frac{d}{\sqrt{2}} (Ω_{1} + i Ω_{2}) = v_{1}$ (because $\sqrt{3 / (8 π)} = d / \sqrt{2}$ ), and $Y_{1, - 1} = + \frac{d}{\sqrt{2}} (Ω_{1} - i Ω_{2}) = v_{- 1}$ .

2.1step 1.1F1algebra

[(b) $L_{3}$ and ladder] Compute the polynomial actions with $D_{1} = x_{2} \partial_{3} - x_{3} \partial_{2}$ , $D_{2} = x_{3} \partial_{1} - x_{1} \partial_{3}$ , $D_{3} = x_{1} \partial_{2} - x_{2} \partial_{1}$ and [F1]: $D_{3} (Ω_{1} \pm i Ω_{2}) = \pm i (Ω_{1} \pm i Ω_{2})$ (since $D_{3} Ω_{1} = - Ω_{2}$ , $D_{3} Ω_{2} = Ω_{1}$ ), hence $L_{3} (Ω_{1} \pm i Ω_{2}) = \pm ℏ (Ω_{1} \pm i Ω_{2})$ and, after the normalisation $v_{\pm 1} = \mp \frac{d}{\sqrt{2}} (Ω_{1} \pm i Ω_{2})$ , $L_{3} v_{1} = ℏ v_{1}$ , $L_{3} v_{- 1} = - ℏ v_{- 1}$ , and $L_{3} v_{0} = 0$ ; further $(D_{1} + i D_{2}) (Ω_{1} + i Ω_{2}) = 0$ , $(D_{1} + i D_{2}) Ω_{3} = - i (Ω_{1} + i Ω_{2})$ , $(D_{1} + i D_{2}) (Ω_{1} - i Ω_{2}) = 2 i Ω_{3}$ , so $L_{+} = - i ℏ (D_{1} + i D_{2})$ satisfies $L_{+} v_{1} = 0$ , $L_{+} v_{0} = - i ℏ d (- i (Ω_{1} + i Ω_{2})) = - ℏ d (Ω_{1} + i Ω_{2}) = \sqrt{2} ℏ v_{1}$ , and $L_{+} v_{- 1} = - i ℏ d \frac{2 i}{\sqrt{2}} Ω_{3} = \sqrt{2} ℏ d Ω_{3} = \sqrt{2} ℏ v_{0}$ ; the relations for $L_{-} ∣_{V_{1}} = (L_{+} ∣_{V_{1}})^{*}$ follow by the finite-block adjunction of [F1].

3.1step 1.1F1F4algebra

[(b) commutators on the core] With the same operators, $L_{1} x_{1} = 0$ , $L_{1} x_{2} = i ℏ x_{3}$ , $L_{1} x_{3} = - i ℏ x_{2}$ ; $L_{2} x_{1} = - i ℏ x_{3}$ , $L_{2} x_{2} = 0$ , $L_{2} x_{3} = i ℏ x_{1}$ ; $L_{3} x_{1} = i ℏ x_{2}$ , $L_{3} x_{2} = - i ℏ x_{1}$ , $L_{3} x_{3} = 0$ . Evaluating $L_{1} L_{2} - L_{2} L_{1}$ on $x_{1}, x_{2}, x_{3}$ : since $L_{2} x_{1} = - i ℏ x_{3}$ and $L_{1} x_{1} = 0$ one has $L_{1} L_{2} x_{1} = - i ℏ L_{1} x_{3} = - ℏ^{2} x_{2}$ and $L_{2} L_{1} x_{1} = 0$ , so $[L_{1}, L_{2}] x_{1} = - ℏ^{2} x_{2} = i ℏ (i ℏ x_{2}) = i ℏ L_{3} x_{1}$ ; $[L_{1}, L_{2}] x_{2} = + ℏ^{2} x_{1} = i ℏ L_{3} x_{2}$ ; and $[L_{1}, L_{2}] x_{3} = 0 = i ℏ L_{3} x_{3}$ . Hence $[L_{1}, L_{2}] = i ℏ L_{3}$ on $V_{1}$ , and cyclically for the other two pairs, consistent with [F1]. Likewise, squaring the displayed actions: $L_{1}^{2} x_{1} = 0$ , $L_{2}^{2} x_{1} = ℏ^{2} x_{1}$ , $L_{3}^{2} x_{1} = ℏ^{2} x_{1}$ ; $L_{1}^{2} x_{2} = i ℏ L_{1} x_{3} = ℏ^{2} x_{2}$ , $L_{2}^{2} x_{2} = 0$ , $L_{3}^{2} x_{2} = ℏ^{2} x_{2}$ ; $L_{1}^{2} x_{3} = ℏ^{2} x_{3}$ , $L_{2}^{2} x_{3} = ℏ^{2} x_{3}$ , $L_{3}^{2} x_{3} = 0$ ; in each case the sum is $2 ℏ^{2} x_{i}$ , so $L_{1}^{2} + L_{2}^{2} + L_{3}^{2} = 2 ℏ^{2} i d$ on $V_{1}$ , which equals $ℏ^{2} A ∣_{V_{1}}$ by [F4]. Alternatively the sum identity follows from the ladder relations of step 2.1 via $L_{1}^{2} + L_{2}^{2} = \frac{1}{2} (L_{+} L_{-} + L_{-} L_{+})$ and $L_{1}^{2} + L_{2}^{2} + L_{3}^{2} = 2 ℏ^{2}$ on each $v_{m}$ .

4.1step 1.1step 2.1step 3.1F4F5algebra∎

[(c) spin-one equivalence] By steps 1.1 and 2.1 the assignment $e_{m} \mapsto v_{m}$ matches the spin-one relations of [F5]: $J_{z} e_{m} = m e_{m}$ with $L_{3} v_{m} = ℏ m v_{m}$ , and $J_{+} e_{1} = 0$ , $J_{+} e_{0} = \sqrt{2} e_{1}$ , $J_{+} e_{- 1} = \sqrt{2} e_{0}$ with $L_{+} v_{1} = 0$ , $L_{+} v_{0} = \sqrt{2} ℏ v_{1}$ , $L_{+} v_{- 1} = \sqrt{2} ℏ v_{0}$ ; since both bases are orthonormal and $L_{x} = \frac{1}{2} (L_{+} + L_{-})$ , $L_{y} = \frac{1}{2 i} (L_{+} - L_{-})$ mirror $J_{x}, J_{y}$ , the assignment is a unitary isomorphism carrying $J_{i}$ to $ℏ^{- 1} L_{i}$ for $i = x, y, z$ . The last assertion is step 3.1 with [F4].

Orbital core commutators

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources