LemmaStatement: 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.

Permutation sector projections on the n-fold tensor power

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space, $n \geq 1$ , and $H^{\otimes n}$ the $n$ -fold completed tensor power ( $H^{\otimes 1} : = H$ , $H^{\otimes (k + 1)} : = H^{\otimes k} \hat{\otimes} H$ as in Hilbert tensor construction: inner product, completion and product bases). For $v_{0}, \dots, v_{n - 1} \in H$ write $v_{0} \otimes \dots \otimes v_{n - 1} \in H^{\otimes n}$ for the iterated elementary tensor.

(a) For every $π$ in the symmetric group $S_{n}$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation) there is a unique unitary $U_{π} \in B (H^{\otimes n})$ with

$U_{π} (v_{0} \otimes \dots \otimes v_{n - 1}) = v_{π^{- 1} (0)} \otimes \dots \otimes v_{π^{- 1} (n - 1)},$

and $U_{π} U_{σ} = U_{π σ}$ , $U_{π}^{*} = U_{π^{- 1}}$ .

(b) The operators

$P_{+} : = \frac{1}{n!} \sum_{π \in S_{n}} U_{π}, P_{-} : = \frac{1}{n!} \sum_{π \in S_{n}} sgn (π) U_{π}$

(with $sgn$ the sign homomorphism, The sign is a homomorphism $S_{n} \to {+ 1, - 1}$ , surjective exactly when $n \geq 2$ ) are orthogonal projections.

(c) $U_{π} P_{+} = P_{+} U_{π} = P_{+}$ and $U_{π} P_{-} = P_{-} U_{π} = sgn (π) P_{-}$ for every $π$ ; consequently the range of $P_{+}$ is the subspace of vectors fixed by every $U_{π}$ , and the range of $P_{-}$ is the subspace of vectors transforming by $sgn$ .

(d) If $v_{0}, \dots, v_{n - 1}$ have a repeated factor, that is, $v_{i} = v_{j}$ for some distinct $i, j \in {0, \dots, n - 1}$ , then $P_{-} (v_{0} \otimes \dots \otimes v_{n - 1}) = 0$ .

Selecting the symmetric or antisymmetric sector for a particle species is a physical postulate, not a theorem of this construction; no spin-statistics statement is proved here.

Facts & Assumptions

Given: A complex Hilbert space $H$ ; $n \geq 1$ ; the tensor powers $H^{\otimes k}$ ; the symmetric group $S_{n}$ and its sign homomorphism.

[F1]

The completed tensor product construction provides: the algebraic tensor product with bilinear elementary tensors, the inner product with $⟨ u \otimes v, u^{'} \otimes v^{'} ⟩ = ⟨ u, u^{'} ⟩ ⟨ v, v^{'} ⟩$ , the dense inclusion, unique orthonormal-coordinate expansions and $∥ u \otimes v ∥ = ∥ u ∥ ∥ v ∥$ (Hilbert tensor construction: inner product, completion and product bases).

[F2]

Bounded operators $S, T$ extend uniquely to $S \otimes T$ with $∥ S \otimes T ∥ \leq ∥ S ∥ ∥ T ∥$ , the adjoint is $S^{*} \otimes T^{*}$ , and compositions multiply; unitary factors have unitary tensor product (Bounded tensor maps: extension, norm estimate, adjoint and commutation).

[F3]

Any parenthesized iterated tensor product represents multilinear maps: for a multilinear map $Φ : H^{n} \to Z$ there is a unique linear $L$ with $L (v_{1} \otimes \dots \otimes v_{n}) = Φ (v_{1}, \dots, v_{n})$ and different parenthesizations agree (Finite iterated tensor products represent multilinear maps independently of parenthesization).

[F4]

$sgn : S_{n} \to {+ 1, - 1}$ is a homomorphism with $sgn (π σ) = sgn (π) sgn (σ)$ and $sgn (π^{- 1}) = sgn (π)$ ; $A_{n} = \ker sgn$ consists of the even permutations (The sign is a homomorphism $S_{n} \to {+ 1, - 1}$ , surjective exactly when $n \geq 2$ , The alternating group $A_{n} = \ker (sgn)$ of even permutations, For $n \geq 2$ , sign is the unique nontrivial homomorphism $S_{n} \to {+ 1, - 1}$ ).

Proof

1.1givenF1F3constructalgebra

[Permutation isometries on the dense algebraic core] The span of iterated elementary tensors is dense in $H^{\otimes n}$ , by induction on the completion construction [F1]. On the algebraic iterated tensor product, the multilinear assignment $(v_{0}, \dots, v_{n - 1}) \mapsto v_{π^{- 1} (0)} \otimes \dots \otimes v_{π^{- 1} (n - 1)}$ induces a linear map by [F3]. It descends isometrically to its image in the completed tensor power: for elementary tensors $v = v_{0} \otimes \dots \otimes v_{n - 1}$ and $w = w_{0} \otimes \dots \otimes w_{n - 1}$ , the inner product of their permuted images is $\prod_{k = 0}^{n - 1} ⟨ v_{π^{- 1} (k)}, w_{π^{- 1} (k)} ⟩ = \prod_{k = 0}^{n - 1} ⟨ v_{k}, w_{k} ⟩ = ⟨ v, w ⟩$ by [F1]. Sesquilinearity gives the same identity for finite linear combinations, so any algebraic relation with zero norm has zero-norm image. The isometry therefore extends uniquely by continuity to $U_{π}$ on the completion. For $n = 1$ it is the identity, and the zero Hilbert space is included.

2.1step 1.1F1F2algebra

[Group law and unitarity] Direct substitution of indices in the elementary formula gives $U_{π} U_{σ} = U_{π σ}$ and $U_{e} = I$ on the dense algebraic core; continuity gives these equalities on the whole completion. Thus $U_{π^{- 1}} U_{π} = I = U_{π} U_{π^{- 1}}$ , so the isometry of step 1.1 is surjective and unitary, with $U_{π}^{*} = U_{π^{- 1}}$ . Any bounded operator with the same elementary action agrees with this one on a dense span and hence everywhere, proving uniqueness. No choice of permutation word or zeroth tensor power is needed.

3.1step 2.1F4algebra

[The projections are orthogonal projections] With coefficients $c_{+} (π) = 1$ and $c_{-} (π) = sgn (π)$ , write $P_{\pm} : = \frac{1}{n!} \sum_{π} c_{\pm} (π) U_{π}$ as in the Statement, use $U_{π} U_{σ} = U_{π σ}$ and reindex $τ = π σ$ : for $P_{+}$ this gives $P_{+}^{2} = \frac{1}{(n!)^{2}} \sum_{π, σ} U_{π σ} = \frac{1}{(n!)^{2}} \sum_{τ} n! U_{τ} = P_{+}$ , and for $P_{-}$ , since $σ = π^{- 1} τ$ and by [F4] $sgn (π) sgn (σ) = sgn (τ)$ , it gives $P_{-}^{2} = \frac{1}{(n!)^{2}} \sum_{π, σ} sgn (π) sgn (σ) U_{π σ} = \frac{1}{(n!)^{2}} \sum_{τ} n! sgn (τ) U_{τ} = P_{-}$ ; moreover $P_{\pm}^{*} = \frac{1}{n!} \sum_{π} c_{\pm} (π) U_{π^{- 1}} = \frac{1}{n!} \sum_{τ} c_{\pm} (τ) U_{τ} = P_{\pm}$ because $U_{π}^{*} = U_{π^{- 1}}$ and $sgn (π^{- 1}) = sgn (π)$ [F4]. Hence $P_{\pm}$ are orthogonal projections.

4.1step 2.1step 3.1F4algebra

[Ranges and transformation laws] For every $π$ , $U_{π} P_{+} = \frac{1}{n!} \sum_{σ} U_{π σ} = \frac{1}{n!} \sum_{τ} U_{τ} = P_{+}$ and $U_{π} P_{-} = \frac{1}{n!} \sum_{σ} sgn (σ) U_{π σ} = sgn (π) \frac{1}{n!} \sum_{τ} sgn (τ) U_{τ} = sgn (π) P_{-}$ , using $sgn (σ) sgn (π σ) = sgn (π)$ [F4]; by self-adjointness of the projections these identities also hold with the order reversed. Consequently, if $u \in ran P_{+}$ then $U_{π} u = P_{+} u = u$ for all $π$ , and if $u \in ran P_{-}$ then $U_{π} u = sgn (π) u$ ; conversely $U_{π} u = u$ for all $π$ gives $P_{+} u = u$ , and $U_{π} u = sgn (π) u$ for all $π$ gives $P_{-} u = \frac{1}{n!} \sum_{π} sgn (π)^{2} u = u$ .

5.1step 2.1step 3.1F4algebra∎

[Vanishing on repeated factors] Suppose $v_{i} = v_{j}$ for distinct $i, j \in {0, \dots, n - 1}$ and let $τ$ be the transposition swapping those positions. Then $U_{τ} (v_{0} \otimes \dots \otimes v_{n - 1}) = v_{0} \otimes \dots \otimes v_{n - 1}$ because the swap exchanges equal vectors. Pairing the terms of the sum defining $n! P_{-}$ as ${π, π τ}$ over a set of coset representatives of the subgroup ${e, τ}$ gives, for each pair, $sgn (π) U_{π} v + sgn (π τ) U_{π τ} v = sgn (π) U_{π} v - sgn (π) U_{π} U_{τ} v = 0$ by $U_{π τ} = U_{π} U_{τ}$ and $U_{τ} v = v$ . Hence $P_{-} v = 0$ for the tensor with a repeated factor.

Permutation sector projections on the n-fold tensor power

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources