LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck 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.

The two-particle exchange operator and the symmetric and antisymmetric combinations

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space with inner product linear in the first argument (Hilbert space, Real and complex inner-product spaces and their induced length), let $H \hat{\otimes} H$ be its completed tensor square with inclusion $κ$ (Hilbert tensor construction: inner product, completion and product bases), and for $n = 2$ let $(U_{π})_{π \in S_{2}}$ and the projections $P_{\pm}^{(2)}$ be those of Permutation sector projections on the n-fold tensor power. Write $τ : = U_{(0 1)}$ for the exchange operator, so that $τ (κ (u \otimes v)) = κ (v \otimes u)$ for $u, v \in H$ ; in the sequel the inclusion is suppressed and $u \otimes v$ denotes $κ (u \otimes v)$ . Then:

(a) $τ$ is self-adjoint and $τ^{2} = I$ ; consequently $τ$ is an isometry with $τ^{- 1} = τ = τ^{*}$ (The Hilbert-space adjoint of a bounded operator, A bounded linear operator between normed spaces);

(b) $P_{+}^{(2)} = \frac{1}{2} (I + τ)$ and $P_{-}^{(2)} = \frac{1}{2} (I - τ)$ , and $ran P_{+}^{(2)} = {x \in H \hat{\otimes} H : τ x = x}, ran P_{-}^{(2)} = {x \in H \hat{\otimes} H : τ x = - x};$

(c) for all $u, v \in H$ , $∥ u \otimes v + v \otimes u ∥^{2} = 2 (∥ u ∥^{2} ∥ v ∥^{2} + ∣ ⟨ u, v ⟩ ∣^{2}), ∥ u \otimes v - v \otimes u ∥^{2} = 2 (∥ u ∥^{2} ∥ v ∥^{2} - ∣ ⟨ u, v ⟩ ∣^{2});$ in particular, if $u, v$ are orthonormal, then $s : = \frac{1}{\sqrt{2}} (u \otimes v + v \otimes u)$ and $a : = \frac{1}{\sqrt{2}} (u \otimes v - v \otimes u)$ are orthonormal, $τ s = s$ and $τ a = - a$ , and both $ran P_{\pm}^{(2)}$ are nonzero;

(d) whenever $u, v \in H$ are orthonormal, $τ κ (u \otimes v) \neq κ (u \otimes v)$ . Consequently, if $H$ contains an orthonormal pair (equivalently, $\dim H \geq 2$ ), both exchange eigenspaces contain nonzero vectors and $τ \neq I$ . If $H = {0}$ or $\dim H = 1$ , then $τ = I$ , $P_{+}^{(2)} = I$ and $P_{-}^{(2)} = 0$ ; for $H = {0}$ the tensor square and both ranges are zero.

Facts & Assumptions

Given: The complex Hilbert space $H$ with inner product linear in the first argument, the completed tensor square $H \hat{\otimes} H$ with inclusion $κ$ , the permutation unitaries $U_{π}$ for $n = 2$ and the projections $P_{\pm}^{(2)}$ , and vectors $u, v \in H$ .

[F1]

Tensor square. $κ : H ⊙ H \to H \hat{\otimes} H$ is a linear isometry with dense image, $κ (u \otimes v)$ is bilinear in $(u, v)$ , $∥ κ (u \otimes v) ∥ = ∥ u ∥ ∥ v ∥$ and $⟨ κ (u \otimes v), κ (u^{'} \otimes v^{'}) ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩$ (Hilbert tensor construction: inner product, completion and product bases clauses (a)-(d), Real and complex inner-product spaces and their induced length).

[F2]

Permutation unitaries. $U_{(0 1)} \in B (H \hat{\otimes} H)$ is the unique bounded operator with $U_{(0 1)} κ (u \otimes v) = κ (v \otimes u)$ ; it is unitary with $U_{π} U_{σ} = U_{π σ}$ and $U_{π}^{*} = U_{π^{- 1}}$ . For every $π \in S_{2}$ , $U_{π} P_{+}^{(2)} = P_{+}^{(2)} U_{π} = P_{+}^{(2)}$ and $U_{π} P_{-}^{(2)} = P_{-}^{(2)} U_{π} = sgn (π) P_{-}^{(2)}$ . The orthogonal projections are $P_{+}^{(2)} = \frac{1}{2} \sum_{π \in S_{2}} U_{π}$ and $P_{-}^{(2)} = \frac{1}{2} \sum_{π \in S_{2}} sgn (π) U_{π}$ (Permutation sector projections on the n-fold tensor power clauses (a)-(c), The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F3]

Orthogonal projections. An orthogonal projection $P$ satisfies $P^{2} = P = P^{*}$ , and its range is a closed subspace (The Hilbert orthogonal projection onto a closed subspace, Hilbert projections are linear, self-adjoint and contractive).

[F4]

Adjoint and operator norm. For $T \in B (H \hat{\otimes} H)$ the Hilbert adjoint $T^{*}$ is the unique bounded operator with $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ , and $T$ is an isometry exactly when $T^{*} T = I$ ; $∥ T x ∥ \leq ∥ T ∥ ∥ x ∥$ (The Hilbert-space adjoint of a bounded operator, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces).

Proof

1.1F2F4algebra

[The exchange operator is a self-adjoint involution] By [F2] with $π = σ = (0 1)$ one has $τ^{2} = U_{(0 1) (0 1)} = U_{e} = I$ , and $τ^{*} = U_{(0 1)^{- 1}} = U_{(0 1)} = τ$ ; hence $τ^{- 1} = τ = τ^{*}$ and $τ$ is an isometry, which is (a).

1.2F2algebra

[The projections in terms of the exchange operator] Since $S_{2} = {e, (0 1)}$ and $sgn (e) = 1$ , $sgn ((0 1)) = - 1$ , the formulas of [F2] give $P_{+}^{(2)} = \frac{1}{2} (U_{e} + U_{(0 1)}) = \frac{1}{2} (I + τ)$ and $P_{-}^{(2)} = \frac{1}{2} (U_{e} - U_{(0 1)}) = \frac{1}{2} (I - τ)$ , which is the first assertion of (b).

2.1step 1.1step 1.2F3algebra

[Eigenspaces as ranges] Let $x \in H \hat{\otimes} H$ . If $τ x = x$ , then $\frac{1}{2} (I + τ) x = x$ , so $x \in ran \frac{1}{2} (I + τ)$ ; conversely if $x = \frac{1}{2} (I + τ) y$ for some $y$ , then $τ x = \frac{1}{2} (τ y + τ^{2} y) = \frac{1}{2} (τ y + y) = x$ by step 1.1. Hence the fixed space of $τ$ is $ran \frac{1}{2} (I + τ) = ran P_{+}^{(2)}$ by step 1.2; the same substitution with $x = \frac{1}{2} (I - τ) y$ gives $τ x = - x$ , and conversely $τ x = - x$ implies $x = \frac{1}{2} (I - τ) x$ , so the $(- 1)$ -eigenspace is $ran P_{-}^{(2)}$ . This completes (b).

2.2F1F2step 1.1algebra

[Norm identities on products] By [F1] the elementary tensors satisfy $∥ u \otimes v ∥^{2} = ∥ u ∥^{2} ∥ v ∥^{2}$ and $⟨ u \otimes v, v \otimes u ⟩ = ⟨ u, v ⟩ ⟨ v, u ⟩ = ∣ ⟨ u, v ⟩ ∣^{2}$ ; expanding $∥ u \otimes v \pm v \otimes u ∥^{2} = ∥ u \otimes v ∥^{2} + ∥ v \otimes u ∥^{2} \pm 2 Re ⟨ u \otimes v, v \otimes u ⟩$ and using that the last number is the real number $∣ ⟨ u, v ⟩ ∣^{2}$ gives the two identities of (c). If $u, v$ are orthonormal then $∥ u ∥ = ∥ v ∥ = 1$ and $⟨ u, v ⟩ = 0$ , so $s$ and $a$ have norm one; moreover $τ s = \frac{1}{\sqrt{2}} (v \otimes u + u \otimes v) = s$ and $τ a = \frac{1}{\sqrt{2}} (v \otimes u - u \otimes v) = - a$ by [F2]; and $⟨ s, a ⟩ = \frac{1}{2} (∥ u \otimes v ∥^{2} - ∥ v \otimes u ∥^{2}) = 0$ , so $s, a$ are orthonormal and $s \neq 0 \neq a$ . This proves (c).

3.1F1F2step 2.2algebraconstruct

[Nonvanishing of the swapped product] Let $u, v$ be orthonormal. Then $u \otimes v$ and $v \otimes u$ are orthonormal in $H \hat{\otimes} H$ : both have norm one by [F1], and $⟨ u \otimes v, v \otimes u ⟩ = ⟨ u, v ⟩ ⟨ v, u ⟩ = 0$ . Hence $v \otimes u \neq u \otimes v$ , so $τ (u \otimes v) \neq u \otimes v$ by [F2]; taking $x : = u \otimes v$ and $x^{'} : = s$ and $x^{''} : = a$ from step 2.2 gives nonzero vectors with $τ x^{'} = x^{'}$ and $τ x^{''} = - x^{''}$ , so $τ \neq I$ . This proves (d).

4.1F1F2step 1.2step 3.1choosealgebra

[Zero and one-dimensional spaces] If $H = {0}$ , all elementary tensors are zero and their completion is zero, so $τ = I$ on that space. If $H$ is one-dimensional, fix a unit spanning vector $e$ . Every elementary tensor has the form $(α e) \otimes (β e) = α β (e \otimes e)$ and its swap is $β α (e \otimes e)$ , the same vector. Hence $τ = I$ on the dense algebraic tensor space and, by boundedness, on its completion. Step 1.2 then gives $P_{+}^{(2)} = I$ and $P_{-}^{(2)} = 0$ in both cases. If $\dim H \geq 2$ , normalize a nonzero vector $u$ and choose $w$ outside its span; the nonzero vector $w - ⟨ w, u ⟩ u$ normalizes to a unit $v$ orthogonal to $u$ , so step 3.1 applies. This proves all branches of (d).

5.1step 1.1step 1.2step 2.1step 2.2step 3.1step 4.1∎

[Assembly] Step 1.1 proves (a), steps 1.2 and 2.1 prove (b), step 2.2 proves (c) and steps 3.1 and 4.1 prove (d). Only the cited tensor and permutation mathematics and the Countable Choice hypothesis of [F2] were used; no physical reading of the exchange operator is asserted.

Remarks

Why the letter $τ$ . The operator is the $n = 2$ instance of the permutation unitaries; the notation $τ$ matches the exchange operator of the source treatments and is used on this pair's pages for the two-particle swap.
Scope. The lemma concerns a single Hilbert space and its tensor square; it asserts nothing about particles, spin, statistics or dynamics. The physical reading of $τ$ as the exchange of two labelled factors is fixed in Declared species sectors and their preparations: the framework's reading of P6 on the page for the identical-particle model.

The two-particle exchange operator and the symmetric and antisymmetric combinations

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources