LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

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.

Singlet pairings: the joint laws of the two spin-half factors along two directions

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), the hypothesis of the tensor construction cited below. Let $V = C^{2}$ carry the orthonormal basis $(e_{+}, e_{-})$ and let $σ_{x} = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), σ_{y} = (\begin{array}{cc} 0 & - i \\ i & 0 \end{array}), σ_{z} = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ be the Pauli matrices of clause (e) of Finite spin matrices in the ordered basis $(e_{+}, e_{-})$ ; for $a = (a_{x}, a_{y}, a_{z}) \in R^{3}$ put $σ_{a} : = a_{x} σ_{x} + a_{y} σ_{y} + a_{z} σ_{z}$ , and for $ε \in Σ = {- 1, + 1}$ put $P_{a, ε} : = \frac{1}{2} (I + ε σ_{a}) .$ Let $V \hat{\otimes} V$ be the completed tensor product with inclusion $κ$ of Hilbert tensor construction: inner product, completion and product bases and let $Ψ : = \frac{1}{\sqrt{2}} (κ (e_{+} \otimes e_{-}) - κ (e_{-} \otimes e_{+})) \in V \hat{\otimes} V, q : = \frac{1}{\sqrt{2}} (κ (e_{+} \otimes e_{-}) + κ (e_{-} \otimes e_{+})) .$ Then:

(a) for every unit $a \in R^{3}$ and $ε \in Σ$ the operator $P_{a, ε}$ is an orthogonal projection on $V$ , $P_{a, +} + P_{a, -} = I$ and $P_{a, ε} P_{a, ε^{'}} = δ_{ε ε^{'}} P_{a, ε}$ ;

(b) $∥ Ψ ∥ = 1$ and the four vectors $Ψ, q, κ (e_{+} \otimes e_{+}), κ (e_{-} \otimes e_{-})$ are mutually orthogonal, so $(Ψ, q, κ (e_{+} \otimes e_{+}), κ (e_{-} \otimes e_{-}))$ is an orthonormal basis of $V \hat{\otimes} V$ ;

(c) for all unit $a, b \in R^{3}$ and all $ε, δ \in Σ$ , $⟨ (P_{a, ε} \otimes P_{b, δ}) Ψ, Ψ ⟩ = \frac{1}{4} (1 - ε δ a \cdot b);$

(d) the marginals of the four numbers in (c) are $\sum_{δ \in Σ} ⟨ (P_{a, ε} \otimes P_{b, δ}) Ψ, Ψ ⟩ = \frac{1}{2} = \sum_{ε \in Σ} ⟨ (P_{a, ε} \otimes P_{b, δ}) Ψ, Ψ ⟩,$ and their correlation is $\sum_{ε \in Σ} \sum_{δ \in Σ} ε δ ⟨ (P_{a, ε} \otimes P_{b, δ}) Ψ, Ψ ⟩ = - a \cdot b .$

The lemma is a finite-dimensional computation in the tensor product; it asserts no preparation, measurement or physical interpretation. The Axiom of Countable Choice enters only through the construction of the completed tensor product cited from Hilbert tensor construction: inner product, completion and product bases.

Facts & Assumptions

Given: The space $V = C^{2}$ with orthonormal basis $(e_{+}, e_{-})$ and the Pauli matrices $σ_{x}, σ_{y}, σ_{z}$ ; unit vectors $a, b \in R^{3}$ ; the completed tensor product $V \hat{\otimes} V$ with inclusion $κ$ ; the vectors $Ψ$ and $q$ ; the labels $ε, δ \in Σ$ ; the Axiom of Countable Choice.

[F1]

The Pauli matrices satisfy $σ_{i}^{*} = σ_{i}$ , $σ_{x}^{2} = σ_{y}^{2} = σ_{z}^{2} = I$ , $σ_{x} σ_{y} = i σ_{z}$ , $σ_{y} σ_{z} = i σ_{x}$ , $σ_{z} σ_{x} = i σ_{y}$ and consequently $σ_{i} σ_{j} + σ_{j} σ_{i} = 2 δ_{i j} I$ ; their actions on the basis are $σ_{x} e_{+} = e_{-}$ , $σ_{x} e_{-} = e_{+}$ , $σ_{y} e_{+} = i e_{-}$ , $σ_{y} e_{-} = - i e_{+}$ , $σ_{z} e_{+} = e_{+}$ and $σ_{z} e_{-} = - e_{-}$ (Finite spin matrices clause (e), Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[F2]

For every $a \in R^{3}$ the matrix $σ_{a} = \sum_{i} a_{i} σ_{i}$ is self-adjoint and $σ_{a}^{2} = \sum_{i, j} a_{i} a_{j} σ_{i} σ_{j} = \sum_{i} a_{i}^{2} I + \sum_{i \neq j} a_{i} a_{j} σ_{i} σ_{j} = ∥ a ∥^{2} I$ by the anticommutation relations of [F1]; in particular $σ_{a}^{2} = I$ for unit $a$ , and $σ_{a}$ is a linear map $V \to V$ (Finite spin matrices clauses (a), (e), Linear map between vector spaces over the same field).

[F3]

The completed tensor product $V \hat{\otimes} V$ is a complex Hilbert space, $κ$ is a linear isometry with dense image, $⟨ κ (u \otimes v), κ (u^{'} \otimes v^{'}) ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩$ for all $u, u^{'}, v, v^{'} \in V$ , and the four elementary tensors $κ (e_{ε} \otimes e_{δ})$ form an orthonormal basis (Hilbert tensor construction: inner product, completion and product bases clauses (b), (c), (d), Real and complex inner product spaces, with the inner product linear in the first argument, Real and complex inner-product spaces and their induced length, Hilbert space, The induced length is a norm).

[F4]

For bounded $S, T$ on $V$ there is a bounded operator $S \otimes T$ on $V \hat{\otimes} V$ with $(S \otimes T) κ (u \otimes v) = κ (S u \otimes T v)$ for all $u, v \in V$ , $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ , and the assignment is linear in each argument (Bounded tensor maps: extension, norm estimate, adjoint and commutation clauses (a), (b), (c)); consequently computations on $Ψ$ may be performed term by term in the orthonormal basis of [F3].

[F5]

In a complex inner product space, $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors); the norm is induced by the inner product, $∥ z ∥ = ⟨ z, z ⟩^{1 / 2}$ (The induced length is a norm, Real and complex inner-product spaces and their induced length).

Proof

technique · direct; verify the projection algebra from the Pauli anticommutation relations, compute the action of the local and product Pauli operators on the four product-basis vectors, read the pairings off the orthonormal basis, and assemble the joint numbers from the projection decomposition

Given: The data of the statement and [F1]-[F5].

1.1givenF2algebra

[Projections] Fix a unit $a$ and $ε \in Σ$ . By [F2], $P_{a, ε}^{*} = \frac{1}{2} (I + ε σ_{a}^{*}) = \frac{1}{2} (I + ε σ_{a}) = P_{a, ε}$ and $P_{a, ε}^{2} = \frac{1}{4} (I + 2 ε σ_{a} + ε^{2} σ_{a}^{2}) = \frac{1}{4} (2 I + 2 ε σ_{a}) = \frac{1}{2} (I + ε σ_{a}) = P_{a, ε}$ using $ε^{2} = 1$ and $σ_{a}^{2} = I$ ; hence $P_{a, ε}$ is an orthogonal projection. Moreover $P_{a, +} + P_{a, -} = I$ and $P_{a, +} P_{a, -} = \frac{1}{4} (I - σ_{a}^{2}) = 0$ , which is (a).

1.2givenF3F5algebra

[Orthonormal basis] By [F3], $∥ Ψ ∥^{2} = \frac{1}{2} (∥ e_{+} \otimes e_{-} ∥^{2} + ∥ e_{-} \otimes e_{+} ∥^{2}) = 1$ and $∥ q ∥^{2} = 1$ , and the inner products pair the four displayed vectors as $0$ or $1$ : for instance $⟨ Ψ, q ⟩ = \frac{1}{2} (1 - 1) = 0$ and $⟨ Ψ, κ (e_{+} \otimes e_{+}) ⟩ = \frac{1}{\sqrt{2}} (⟨ e_{+}, e_{+} ⟩ ⟨ e_{-}, e_{+} ⟩ - ⟨ e_{-}, e_{+} ⟩ ⟨ e_{+}, e_{+} ⟩) = 0$ by the product formula of [F3]. Since the four elementary tensors already form an orthonormal basis of the four-dimensional space $V \hat{\otimes} V$ , so do the four mutually orthogonal unit vectors $Ψ, q, κ (e_{+} \otimes e_{+}), κ (e_{-} \otimes e_{-})$ ; this is (b).

2.1givenF1F4step 1.2algebra

[Local Pauli operators on $Ψ$ ] Using [F1] and [F4] term by term, $(σ_{z} \otimes I) Ψ = \frac{1}{\sqrt{2}} (κ (e_{+} \otimes e_{-}) + κ (e_{-} \otimes e_{+})) = q$ and $(I \otimes σ_{z}) Ψ = \frac{1}{\sqrt{2}} (- κ (e_{+} \otimes e_{-}) - κ (e_{-} \otimes e_{+})) = - q$ ; further $(σ_{x} \otimes I) Ψ = \frac{1}{\sqrt{2}} (κ (e_{-} \otimes e_{-}) - κ (e_{+} \otimes e_{+}))$ , $(I \otimes σ_{x}) Ψ = \frac{1}{\sqrt{2}} (κ (e_{+} \otimes e_{+}) - κ (e_{-} \otimes e_{-}))$ , $(σ_{y} \otimes I) Ψ = \frac{i}{\sqrt{2}} (κ (e_{+} \otimes e_{+}) + κ (e_{-} \otimes e_{-}))$ and $(I \otimes σ_{y}) Ψ = \frac{- i}{\sqrt{2}} (κ (e_{+} \otimes e_{+}) + κ (e_{-} \otimes e_{-}))$ , all of which are linear combinations of the three basis vectors $q, κ (e_{+} \otimes e_{+}), κ (e_{-} \otimes e_{-})$ orthogonal to $Ψ$ by step 1.2; hence $⟨ (σ_{i} \otimes I) Ψ, Ψ ⟩ = 0 = ⟨ (I \otimes σ_{i}) Ψ, Ψ ⟩$ for $i = x, y, z$ , and by the linearity of [F4] in the first tensor argument, $⟨ (σ_{a} \otimes I) Ψ, Ψ ⟩ = 0 = ⟨ (I \otimes σ_{b}) Ψ, Ψ ⟩$ for all $a, b$ .

2.2givenF1F4step 1.2algebra

[Product Pauli operators on $Ψ$ ] Term-by-term application of [F1] and [F4] gives $(σ_{x} \otimes σ_{x}) Ψ = (σ_{y} \otimes σ_{y}) Ψ = (σ_{z} \otimes σ_{z}) Ψ = - Ψ$ . Put $r_{+} : = (κ (e_{+} \otimes e_{+}) + κ (e_{-} \otimes e_{-})) / \sqrt{2}$ and $r_{-} : = (κ (e_{+} \otimes e_{+}) - κ (e_{-} \otimes e_{-})) / \sqrt{2}$ . The six mixed products are $(σ_{x} \otimes σ_{y}) Ψ = - i q$ , $(σ_{y} \otimes σ_{x}) Ψ = i q$ , $(σ_{x} \otimes σ_{z}) Ψ = - r_{+}$ , $(σ_{z} \otimes σ_{x}) Ψ = r_{+}$ , $(σ_{y} \otimes σ_{z}) Ψ = i r_{-}$ and $(σ_{z} \otimes σ_{y}) Ψ = - i r_{-}$ . Each is orthogonal to $Ψ$ by step 1.2. Thus $⟨ (σ_{i} \otimes σ_{j}) Ψ, Ψ ⟩ = - δ_{i j}$ for all $i, j \in {x, y, z}$ .

3.1step 2.2F4algebra

[Directional correlation] By the linearity of [F4], $(σ_{a} \otimes σ_{b}) Ψ = \sum_{i, j} a_{i} b_{j} (σ_{i} \otimes σ_{j}) Ψ$ , so the final identity of step 2.2 and the conjugate-linearity of the inner product in its second argument give $⟨ (σ_{a} \otimes σ_{b}) Ψ, Ψ ⟩ = \sum_{i, j} a_{i} b_{j} (- δ_{i j}) = - a \cdot b$ , with real $a, b$ .

4.1step 1.1step 1.2step 2.1step 3.1F4algebra

[Joint numbers] Let $a, b$ be unit vectors and $ε, δ \in Σ$ . By step 1.1, $P_{a, ε} = \frac{1}{2} (I + ε σ_{a})$ and $P_{b, δ} = \frac{1}{2} (I + δ σ_{b})$ , so multilinearity of the tensor product [F4] and the bilinearity of the inner product give $⟨ (P_{a, ε} \otimes P_{b, δ}) Ψ, Ψ ⟩ = \frac{1}{4} (⟨ Ψ, Ψ ⟩ + ε ⟨ (σ_{a} \otimes I) Ψ, Ψ ⟩ + δ ⟨ (I \otimes σ_{b}) Ψ, Ψ ⟩ + ε δ ⟨ (σ_{a} \otimes σ_{b}) Ψ, Ψ ⟩) = \frac{1}{4} (1 - ε δ a \cdot b)$ by steps 1.2, 2.1 and 3.1; this is (c).

5.1step 4.1algebra

[Marginals and correlation] Summing the formula of step 4.1 over the distant label and using $\sum_{δ \in Σ} δ = 0$ gives $\sum_{δ} ⟨ (P_{a, ε} \otimes P_{b, δ}) Ψ, Ψ ⟩ = \frac{1}{4} (2 - ε a \cdot b \cdot 0) = \frac{1}{2}$ , and symmetrically for the other marginal; the correlation is $\sum_{ε, δ} ε δ \frac{1}{4} (1 - ε δ a \cdot b) = \frac{1}{4} ((\sum_{ε} ε) (\sum_{δ} δ) - a \cdot b \sum_{ε, δ} (ε δ)^{2}) = \frac{1}{4} (0 - 4 a \cdot b) = - a \cdot b$ ; this is (d).

6.1step 1.1step 1.2step 4.1step 5.1∎

[Assembly] Step 1.1 is (a), step 1.2 is (b), step 4.1 is (c) and step 5.1 is (d); only the finite-dimensional tensor calculus of [F1]-[F4] and real arithmetic were used, and no physical interpretation is asserted.

Remarks

Relation to the framework's singlet. The vector $Ψ$ is the singlet of the two-factor spin-half model; its joint numbers (c) are the pairings of the local spin projections, and (d) shows that each single-station marginal is $\frac{1}{2}$ and that the directional correlation is $- a \cdot b$ . The physical reading of these numbers as outcome laws of a declared preparation is fixed on the page of this pair; this lemma itself is linear algebra.
No degenerate directions. The computation covers every pair of unit directions, including $a = b$ (correlation $- 1$ ) and $a = - b$ (correlation $+ 1$ ) and $a ⊥ b$ (correlation $0$ ); the joint numbers are $\frac{1}{4} (1 \mp ε δ)$ in these cases and remain in $[0, 1]$ .

Singlet pairings: the joint laws of the two spin-half factors along two directions

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources