SigmaLayer/Symmetrization: the two-particle symmetrization postulate (identical particles)

Category: 7-SigmaLayer (the projective-sector layer (Paper C)) — the identical-particle / exchange-statistics pillar.

For two identical particles the joint Hilbert space is H ⊗ H, realised concretely as EuclideanSpace ℂ (Fin N × Fin N) (functions on ordered pairs). Particle EXCHANGE is the swap operator (swap x)(i,j) = x(j,i). This module builds the symmetrization postulate at n = 2:

• swap is a self-adjoint involution (swap_involutive, swap_isSymmetric) — a genuine ±1-valued exchange observable;
• the symmetric/antisymmetric projectors symProj = ½(1 + swap), antisymProj = ½(1 − swap) are complementary orthogonal projections summing to the identity (symProj_idem, antisymProj_idem, symProj_antisymProj, symProj_add_antisymProj, and symmetry of each);
• the exchange dichotomy: the symmetric subspace is exactly the +1 eigenspace of swap and the antisymmetric subspace the −1 eigenspace (swap_eq_self_iff, swap_eq_neg_iff), and the two intersect only in 0 (eq_zero_of_swap_self_and_neg) — so H ⊗ H = Sym ⊕ Anti (bosons ⊕ fermions);
• Pauli exclusion: a product state of two particles in the SAME single-particle state v has zero antisymmetric component, antisymProj (v ⊗ v) = 0 (antisymProj_tprod_self) — no two fermions occupy the same state.

This is the finite-dimensional n = 2 core of the symmetrization postulate (the exchange-statistics pillar); the general-n symmetric group action / exterior-power Fock structure is a further extension.

References: SigmaLayer/TensorReconstruction.lean (composite two-system structure); specs/future-work.md (identical-particle statistics). Uses Mathlib LinearIsometryEquiv.piLpCongrLeft, LinearMap.IsSymmetric.

@[reducible, inline]

abbrev CSD.SigmaLayer.TwoParticle (N : ℕ) : Type

The two-particle Hilbert space H ⊗ H for H = ℂ^N, realised as functions on ordered pairs.

Equations

• CSD.SigmaLayer.TwoParticle N = EuclideanSpace ℂ (Fin N × Fin N)

noncomputable def CSD.SigmaLayer.exchangeEquiv (N : ℕ) : TwoParticle N ≃ₗᵢ[ℂ] TwoParticle N

Particle exchange as a linear isometry. The unitary that swaps the two tensor factors, (x)(i,j) ↦ x(j,i), from Equiv.prodComm via piLpCongrLeft.

Equations

• CSD.SigmaLayer.exchangeEquiv N = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (Equiv.prodComm (Fin N) (Fin N))

noncomputable def CSD.SigmaLayer.swap (N : ℕ) : TwoParticle N →ₗ[ℂ] TwoParticle N

The exchange (swap) operator. Particle exchange as an endomorphism of H ⊗ H.

Equations

• CSD.SigmaLayer.swap N = ↑(CSD.SigmaLayer.exchangeEquiv N).toLinearEquiv

theorem CSD.SigmaLayer.exchangeEquiv_symm {N : ℕ} : (exchangeEquiv N).symm = exchangeEquiv N

theorem CSD.SigmaLayer.exchangeEquiv_involutive {N : ℕ} (x : TwoParticle N) : (exchangeEquiv N) ((exchangeEquiv N) x) = x

@[simp]

theorem CSD.SigmaLayer.swap_involutive {N : ℕ} (x : TwoParticle N) : (swap N) ((swap N) x) = x

Exchange is an involution: swapping twice is the identity (swap² = 1).

theorem CSD.SigmaLayer.swap_isSymmetric {N : ℕ} : (swap N).IsSymmetric

Exchange is self-adjoint: a self-inverse unitary, so swap† = swap. Hence the exchange observable has real (±1) spectrum.

The symmetric and antisymmetric projectors

noncomputable def CSD.SigmaLayer.symProj (N : ℕ) : TwoParticle N →ₗ[ℂ] TwoParticle N

The symmetric (bosonic) projector ½(1 + swap).

Equations

• CSD.SigmaLayer.symProj N = (1 / 2) • (LinearMap.id + CSD.SigmaLayer.swap N)

noncomputable def CSD.SigmaLayer.antisymProj (N : ℕ) : TwoParticle N →ₗ[ℂ] TwoParticle N

The antisymmetric (fermionic) projector ½(1 − swap).

Equations

• CSD.SigmaLayer.antisymProj N = (1 / 2) • (LinearMap.id - CSD.SigmaLayer.swap N)

@[simp]

theorem CSD.SigmaLayer.symProj_apply {N : ℕ} (x : TwoParticle N) : (symProj N) x = (1 / 2) • (x + (swap N) x)

@[simp]

theorem CSD.SigmaLayer.antisymProj_apply {N : ℕ} (x : TwoParticle N) : (antisymProj N) x = (1 / 2) • (x - (swap N) x)

theorem CSD.SigmaLayer.symProj_idem {N : ℕ} (x : TwoParticle N) : (symProj N) ((symProj N) x) = (symProj N) x

theorem CSD.SigmaLayer.antisymProj_idem {N : ℕ} (x : TwoParticle N) : (antisymProj N) ((antisymProj N) x) = (antisymProj N) x

theorem CSD.SigmaLayer.symProj_add_antisymProj {N : ℕ} (x : TwoParticle N) : (symProj N) x + (antisymProj N) x = x

The two projectors sum to the identity: every two-particle state splits into a symmetric and an antisymmetric part.

theorem CSD.SigmaLayer.symProj_antisymProj {N : ℕ} (x : TwoParticle N) : (symProj N) ((antisymProj N) x) = 0

The projectors are orthogonal (their product is zero): the symmetric and antisymmetric sectors are complementary.

theorem CSD.SigmaLayer.symProj_isSymmetric {N : ℕ} : (symProj N).IsSymmetric

Each projector is self-adjoint — so Sym ⊕ Anti is an ORTHOGONAL direct sum.

theorem CSD.SigmaLayer.antisymProj_isSymmetric {N : ℕ} : (antisymProj N).IsSymmetric

The exchange dichotomy: Sym = (+1)-eigenspace, Anti = (−1)-eigenspace

theorem CSD.SigmaLayer.swap_eq_self_iff {N : ℕ} (x : TwoParticle N) : (swap N) x = x ↔ (symProj N) x = x

The symmetric subspace is the +1 eigenspace of exchange: a state is exchange-symmetric iff it is fixed by symProj (a boson).

theorem CSD.SigmaLayer.swap_eq_neg_iff {N : ℕ} (x : TwoParticle N) : (swap N) x = -x ↔ (antisymProj N) x = x

The antisymmetric subspace is the −1 eigenspace of exchange: a state is exchange-antisymmetric iff it is fixed by antisymProj (a fermion).

theorem CSD.SigmaLayer.eq_zero_of_swap_self_and_neg {N : ℕ} (x : TwoParticle N) (h1 : (swap N) x = x) (h2 : (swap N) x = -x) : x = 0

The two sectors meet only in 0: no nonzero state is both exchange-symmetric and exchange-antisymmetric. With symProj_add_antisymProj, this makes H ⊗ H = Sym ⊕ Anti a genuine direct sum (bosons ⊕ fermions).

Product states and Pauli exclusion

noncomputable def CSD.SigmaLayer.tprod {N : ℕ} (v w : EuclideanSpace ℂ (Fin N)) : TwoParticle N

A product (unentangled) two-particle state v ⊗ w: (i,j) ↦ vᵢ wⱼ.

Equations

• CSD.SigmaLayer.tprod v w = (WithLp.equiv 2 (Fin N × Fin N → ℂ)).symm fun (p : Fin N × Fin N) => v.ofLp p.1 * w.ofLp p.2

@[simp]

theorem CSD.SigmaLayer.tprod_apply {N : ℕ} (v w : EuclideanSpace ℂ (Fin N)) (p : Fin N × Fin N) : (tprod v w).ofLp p = v.ofLp p.1 * w.ofLp p.2

theorem CSD.SigmaLayer.swap_apply {N : ℕ} (x : TwoParticle N) (p : Fin N × Fin N) : ((swap N) x).ofLp p = x.ofLp (p.2, p.1)

theorem CSD.SigmaLayer.swap_tprod {N : ℕ} (v w : EuclideanSpace ℂ (Fin N)) : (swap N) (tprod v w) = tprod w v

Exchange swaps the two factors of a product state: swap (v ⊗ w) = w ⊗ v.

theorem CSD.SigmaLayer.antisymProj_tprod_self {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : (antisymProj N) (tprod v v) = 0

Pauli exclusion (n = 2). A product state of two identical particles in the SAME single-particle state v is exchange-symmetric, so its antisymmetric (fermionic) component vanishes: antisymProj (v ⊗ v) = 0. No two fermions occupy the same state.