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.

Slater direct and exchange calculation

Statement

Slot convention. For $ℓ \geq 1$ , $S_{ℓ}$ acts on ${0, \dots, ℓ - 1}$ as in Permutation sector projections on the n-fold tensor power. On one-based tuple positions use $\hat{π} (k) : = 1 + π (k - 1)$ for $1 \leq k \leq ℓ$ . Conjugation by $k \mapsto k - 1$ gives $\hat{π σ} = \hat{π} \circ \hat{σ}$ and $\hat{π^{- 1}} = {\hat{π}}^{- 1}$ ; thus the supplier's tensor action becomes $U_{π} (v_{1} \otimes \dots \otimes v_{ℓ}) = v_{{\hat{π}}^{- 1} (1)} \otimes \dots \otimes v_{{\hat{π}}^{- 1} (ℓ)}$ . The parameters of $U_{π}$ and $sgn (π)$ remain canonical zero-based permutations.

Assume the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice). Let $H$ be a complex Hilbert space with completed tensor powers $H^{\otimes n}$ and symmetric projections $P_{\pm}^{(n)}$ (Hilbert tensor construction: inner product, completion and product bases, Permutation sector projections on the n-fold tensor power). Then:

(a) Slater vectors: for $n \geq 2$ and orthonormal $u_{1}, \dots, u_{n} \in H$ , the Slater vector $S (u_{1}, \dots, u_{n}) : = \frac{1}{\sqrt{n!}} \sum_{σ \in S_{n}} sgn (σ) u_{\hat{σ} (1)} \otimes \dots \otimes u_{\hat{σ} (n)}$ satisfies $∥ S (u_{1}, \dots, u_{n}) ∥ = 1$ and $S (u_{1}, \dots, u_{n}) = \sqrt{n!} P_{-}^{(n)} (u_{1} \otimes \dots \otimes u_{n})$ ;

(b) exclusion: if $u_{i} = u_{j}$ for some $i \neq j$ , then $P_{-}^{(n)} (u_{1} \otimes \dots \otimes u_{n}) = 0$ (Permutation sector projections on the n-fold tensor power (d));

(c) two orbitals, bounded pair interaction: let $u, v \in L^{2} (R^{3}; C)$ be normalized and orthogonal, let $W : R^{3} \to R$ be measurable and bounded with $W (- z) = W (z)$ for a.e. $z$ , let $Θ : L^{2} (R^{3}) \otimes L^{2} (R^{3}) \to L^{2} (R^{6})$ be the Euclidean product unitary (Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b})), put $φ_{\pm} : = (u \otimes v \pm v \otimes u) / \sqrt{2}$ and $D : = \int_{R^{6}} ∣ u (x) ∣^{2} ∣ v (y) ∣^{2} W (x - y) d x d y, X : = \int_{R^{6}} \overline{u (x)} v (x) u (y) \overline{v (y)} W (x - y) d x d y,$ integrals of absolutely integrable functions. Then $D, X \in R$ and the pair expectation of the multiplier $M_{W}$ in the two spatial states is $⟨ M_{W} (Θ φ_{\pm}), Θ φ_{\pm} ⟩ = D \pm X .$

(d) repulsive Coulomb exchange: let $κ > 0$ , $W (z) = κ / ∣ z ∣$ , let $u, v \in W^{1, 2} (R^{3}; C) \cap L^{2}$ be normalized and orthogonal (Integer-order Sobolev spaces and their norms, The space $L^{p} (μ)$ as the quotient by null functions). The vectors $Θ φ_{\pm}$ belong to $D (M_{W})$ : Hardy translated in the $y$ variable and Tonelli give $\iint ∣ u (x) v (y) ∣^{2} / ∣ x - y ∣^{2} \leq 4 ∥ u ∥_{2}^{2} ∥ \nabla v ∥_{2}^{2} < \infty$ , and the swapped product has the same property. Then the integrals $D$ and $X$ converge absolutely, $0 \leq D < \infty$ , $X \in R$ with $X \geq 0$ ; consequently $D - X \leq D + X$ , i.e. the antisymmetric spatial pair state has the lower expectation of the repulsive Coulomb pair interaction.

The exchange calculation is a statement about the indicated spatial vectors; it does not deduce the spin-statistics assignment of any species, and combining the spatial states with spin requires a separately stipulated symmetry rule. No physical interpretation of $D$ , $X$ or the states is asserted.

Facts & Assumptions

Given: orthonormal vectors $u_{1}, \dots, u_{n} \in H$ , normalized orthogonal $u, v \in L^{2} (R^{3}; C)$ , a bounded measurable even $W$ , the pair multiplier $M_{W}$ on $L^{2} (R^{6})$ , the numbers $D, X$ , and $κ > 0$ .

[F1]

The permutation unitaries satisfy $U_{π} (v_{1} \otimes \dots \otimes v_{n}) = v_{{\hat{π}}^{- 1} (1)} \otimes \dots \otimes v_{{\hat{π}}^{- 1} (n)}$ , $P_{-}^{(n)} = \frac{1}{n!} \sum_{π} sgn (π) U_{π}$ , and $P_{-}^{(n)} (u_{1} \otimes \dots \otimes u_{n}) = 0$ whenever two of the $u_{i}$ coincide; elementary tensors have norm $∥ v_{1} \otimes \dots \otimes v_{n} ∥ = ∥ v_{1} ∥ \dots ∥ v_{n} ∥$ (Permutation sector projections on the n-fold tensor power, Hilbert tensor construction: inner product, completion and product bases).

[F2]

Cauchy-Schwarz and the $L^{2}$ product structure: for $f, g \in L^{2}$ , $∥ f g ∥_{1} \leq ∥ f ∥_{2} ∥ g ∥_{2}$ , and for bounded measurable $W$ , $∣ W (x - y) ∣ \leq ∥ W ∥_{\infty}$ (Cauchy-Schwarz inequality for $L^{2}$ , The space $L^{p} (μ)$ as the quotient by null functions, Complex Lp classes and Euclidean test-function conventions).

[F3]

Hardy for $W^{1, 2} (R^{3})$ : $∥ w / ∣ \cdot ∣ ∥_{2} \leq 2 ∥ \nabla w ∥_{2}$ (Three-dimensional Hardy bound (c)).

[F4]

Gaussian integrals and transforms: $\int_{R} e^{- s^{2}} d s = \sqrt{π}$ ; for $t > 0$ the Euclidean Fourier transform of $G_{t} (x) : = e^{- t ∣ x ∣^{2}}$ is $\hat{G_{t}} (ξ) = (π / t)^{3 / 2} e^{- π^{2} ∣ ξ ∣^{2} / t} > 0$ ; the identity $1 / r = π^{- 1 / 2} \int_{0}^{\infty} s^{- 1 / 2} e^{- s r^{2}} d s$ for $r > 0$ follows by the substitution $s = u^{2} / r^{2}$ (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ , Euclidean Gaussian transform with the 2π normalization, Plancherel theorem).

[F5]

Tonelli for $σ$ -finite product spaces permits the interchange of the order of integration for nonnegative measurable integrands (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F6]

The Euclidean product unitary $Θ$ satisfies $Θ (f \otimes g) (x, y) = f (x) g (y)$ ; because $M_{W}$ acts on $L^{2} (R^{6})$ , the spatial pairing is $⟨ M_{W} Θ (f \otimes g), Θ (f^{'} \otimes g^{'}) ⟩ = \int f (x) g (y) W (x - y) \overline{f^{'} (x) g^{'} (y)} d x d y$ , in the inner product linear in the first argument (Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b})). Once Tonelli establishes absolute integrability, Fubini applies separately to real and imaginary parts (Fubini's theorem for L^1 functions on a sigma-finite product).

Proof

1.1F1algebra

[Slater norm and identity] For $σ, π \in S_{n}$ , the tensor inner product is $⟨ u_{\hat{σ} (1)} \otimes \dots \otimes u_{\hat{σ} (n)}, u_{\hat{π} (1)} \otimes \dots \otimes u_{\hat{π} (n)} ⟩ = \prod_{i = 1}^{n} ⟨ u_{\hat{σ} (i)}, u_{\hat{π} (i)} ⟩$ by [F1], which equals $1$ if $σ = π$ and $0$ otherwise because the $u_{i}$ are orthonormal. Hence the $n!$ summands of $\sqrt{n!} S$ are mutually orthogonal of norm $1$ , so $∥ \sqrt{n!} S ∥^{2} = n!$ and $∥ S ∥ = 1$ . Moreover $P_{-}^{(n)} (u_{1} \otimes \dots \otimes u_{n}) = \frac{1}{n!} \sum_{π} sgn (π) u_{\hat{π} (1)} \otimes \dots \otimes u_{\hat{π} (n)} = \frac{1}{\sqrt{n!}} S$ , using $U_{π} (u_{1} \otimes \dots \otimes u_{n}) = u_{{\hat{π}}^{- 1} (1)} \otimes \dots \otimes u_{{\hat{π}}^{- 1} (n)}$ and reindexing $π \mapsto π^{- 1}$ . This proves (a).

1.2F1

[Exclusion] The assertion (b) is exactly [F1]'s vanishing statement for $P_{-}^{(n)}$ on a tensor with two equal factors; in particular for $n = 2$ , $P_{-}^{(2)} (u \otimes u) = 0$ .

1.3F2F6algebra

[Two-orbital expansion] Assume the hypotheses of (c). Absolute integrability of the four products $∣ u (x) ∣^{2} ∣ v (y) ∣^{2} ∣ W (x - y) ∣$ , $∣ \overline{u (x)} v (x) u (y) \overline{v (y)} W (x - y) ∣, \dots$ follows from [F2]: e.g. $\int \int ∣ u (x) ∣^{2} ∣ v (y) ∣^{2} ∣ W ∣ \leq ∥ W ∥_{\infty} ∥ u ∥_{2}^{2} ∥ v ∥_{2}^{2} = ∥ W ∥_{\infty}$ and $\int \int ∣ \overline{u} v ∣ ∣ u \overline{v} ∣ ∣ W ∣ \leq ∥ W ∥_{\infty} (\int ∣ u v ∣)^{2} \leq ∥ W ∥_{\infty} ∥ u ∥_{2}^{2} ∥ v ∥_{2}^{2}$ . Expanding the four terms in the tensor representation of [F6] gives $⟨ M_{W} Θ φ_{\pm}, Θ φ_{\pm} ⟩ = \frac{1}{2} [D \pm 2 Re X + D^{'}]$ , where $D^{'} = \int \int ∣ v (x) ∣^{2} ∣ u (y) ∣^{2} W (x - y)$ ; replacing $(x, y)$ by $(y, x)$ and using $W (x - y) = W (y - x)$ gives $D^{'} = D$ , so the expectation is $D \pm Re X$ . Since $W$ is real and even, exchanging the two integration variables in $X$ shows $X = \overline{X}$ , so $X \in R$ and $Re X = X$ ; the same symmetry with real $W$ gives $D \in R$ . This proves (c).

1.4F3F5algebra

[Absolute convergence for the Coulomb kernel] Assume the hypotheses of (d). For the direct term, by [F3] applied in the $y$ -variable for a.e. $x$ and Cauchy-Schwarz, $\int ∣ v (y) ∣^{2} / ∣ x - y ∣ d y \leq 2 ∥ v ∥_{2} ∥ \nabla v ∥_{2} < \infty$ , so with Tonelli [F5] $\int \int \frac{∣ u (x) ∣^{2} ∣ v (y) ∣^{2}}{∣ x - y ∣} = \int ∣ u (x) ∣^{2} (\int \frac{∣ v (y) ∣^{2}}{∣ x - y ∣} d y) d x \leq 2 ∥ v ∥_{2} ∥ \nabla v ∥_{2} ∥ u ∥_{2}^{2} < \infty$ . For the crossed term use $2 ∣ u (x) v (y) v (x) u (y) ∣ \leq ∣ u (x) v (y) ∣^{2} + ∣ v (x) u (y) ∣^{2}$ and the same bound to conclude $\iint \frac{∣ \overline{u (x)} v (x) u (y) \overline{v (y)} ∣}{∣ x - y ∣} < \infty$ . Hence $D, X$ are absolutely convergent and $D = κ \int \int ∣ u ∣^{2} ∣ v ∣^{2} / ∣ x - y ∣ \geq 0$ .

2.1F2F4F5F6step 1.4algebra

[Gaussian positivity with only $L^{1}$ data] Put $f = \overline{u} v \in L^{1}$ by [F2], with no assumption that $f \in L^{2}$ . Step 1.4 gives $\iint ∣ f (x) f (y) ∣ / ∣ x - y ∣ < \infty$ . The Gaussian representation [F4], Tonelli on absolute values [F5] and complex Fubini [F6] therefore give $X = κ π^{- 1 / 2} \int_{0}^{\infty} s^{- 1 / 2} I_{s} d s$ , where $I_{s} : = \iint f (x) \overline{f (y)} e^{- s ∣ x - y ∣^{2}} d x d y$ . For $s > 0$ completion of the square and the three-dimensional Gaussian integral give $e^{- s ∣ x - y ∣^{2}} = (4 s / π)^{3 / 2} \int_{R^{3}} e^{- 2 s ∣ x - z ∣^{2}} e^{- 2 s ∣ y - z ∣^{2}} d z$ . The triple integral of its absolute integrand is $(π / (4 s))^{3 / 2} \iint ∣ f (x) f (y) ∣ e^{- s ∣ x - y ∣^{2}} d x d y \leq (π / (4 s))^{3 / 2} ∥ f ∥_{1}^{2}$ , finite by Tonelli. Complex Fubini then yields $I_{s} = (4 s / π)^{3 / 2} \int_{R^{3}} ∣ \int f (x) e^{- 2 s ∣ x - z ∣^{2}} d x ∣^{2} d z \geq 0$ . The outer integral is absolutely convergent by the first bound from step 1.4 and the Gaussian kernel identity, so $X \geq 0$ and is real. Since $D \geq 0$ , the two absolutely convergent interaction expectations satisfy $D - X \leq D + X$ under the full original $W^{1, 2}$ hypotheses.

3.1step 1.1step 1.2step 1.3step 1.4step 2.1algebra∎

[Conclusion and scope] Steps 1.1 and 1.2 prove (a) and (b), steps 1.3 and 1.4 prove (c), and step 2.1 proves (d). The final paragraph of the statement records that the spin-statistics assignment and any physical interpretation are separate assumptions: the symmetric ( $+$ ) and antisymmetric ( $-$ ) spatial vectors are mathematical vectors, and combining them with spin requires a stipulated symmetry rule. This completes the proof.

Slater direct and exchange calculation

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources