Pauli Exclusion Principle

rigorous Lean 4 verified

Depends On

Lean 4 Verified — 1 result, 1 Lean theorem

The results below have been independently checked in Lean 4, a proof assistant that mechanically verifies every logical step. Click a result name to jump to it in the derivation.

Theorem 4.1 1 Lean theorem
ObserverCentrism.Particles.SpinStatistics
  • pauli_exclusion_core
View Lean source →

Overview

This derivation answers a deceptively simple question: why can’t two identical electrons occupy the same quantum state?

The Pauli exclusion principle is one of the most consequential rules in physics. It explains why atoms have shell structure, why the periodic table exists, why matter is rigid rather than collapsing, and why white dwarf stars can resist gravitational collapse. In standard quantum mechanics, the principle is either postulated directly or derived from quantum field theory. Here it emerges from pure algebra.

The approach. The argument is short and decisive:

The result. The exclusion principle is not an independent law but an algebraic identity: antisymmetry plus same-state exchange equals zero. The derivation extends to show that at most d identical fermions can coexist in a d-dimensional state space, producing atomic shell structure and degeneracy pressure.

Why this matters. The stability of all ordinary matter — atoms, molecules, stars — rests on this single algebraic fact. The derivation shows that this stability is not a contingent feature of our universe’s laws but a necessary consequence of the topological classification of particle types in three spatial dimensions.

An honest caveat. The algebraic core is a tautology of linear algebra. The substantive physics enters through the upstream spin-statistics connection, which establishes the antisymmetry. This derivation packages the consequence; the heavy lifting is in the spin-statistics derivation.

Statement

Theorem. Two identical fermions cannot occupy the same quantum state. This is not an additional postulate but an algebraic consequence of the antisymmetry of fermionic relational invariants (from Spin and Statistics): if I12I_{12} is antisymmetric under exchange and the exchange is trivial (same state), then I12=0I_{12} = 0 — the configuration is coherence-forbidden.

Derivation

Step 1: Setup and Definitions

Definition 1.1. Let H\mathcal{H} be the single-particle Hilbert space of states for a fermion species. A two-fermion state is a vector in HH\mathcal{H} \otimes \mathcal{H}. The exchange operator P12:HHHHP_{12}: \mathcal{H} \otimes \mathcal{H} \to \mathcal{H} \otimes \mathcal{H} is the linear map defined by P12(ψϕ)=ϕψP_{12}(|\psi\rangle \otimes |\phi\rangle) = |\phi\rangle \otimes |\psi\rangle.

Definition 1.2. The relational invariant I12I_{12} of two identical observers O1,O2\mathcal{O}_1, \mathcal{O}_2 in states ψ1,ψ2H|\psi_1\rangle, |\psi_2\rangle \in \mathcal{H} is a function on HH\mathcal{H} \otimes \mathcal{H} encoding the joint coherence structure of the pair. Physically, I12I_{12} is the outcome of a Type III interaction between O1\mathcal{O}_1 and O2\mathcal{O}_2 (from Relational Invariants).

Step 2: Antisymmetry from Spin-Statistics

Proposition 2.1. For identical fermions (half-integer winding class [1]π1(SO(3))=Z2[1] \in \pi_1(SO(3)) = \mathbb{Z}_2), the relational invariant is antisymmetric under exchange:

I12(ψ1,ψ2)=I12(ψ2,ψ1)I_{12}(|\psi_1\rangle, |\psi_2\rangle) = -I_{12}(|\psi_2\rangle, |\psi_1\rangle)

Proof. This is Proposition 4.1 of Spin and Statistics. The exchange phase for winding class [1][1] is eiϕ=(1)1=1e^{i\phi} = (-1)^1 = -1. The relational invariant, as a function on Σ1×Σ2\Sigma_1 \times \Sigma_2, inherits this phase under the swap (ψ1,ψ2)(ψ2,ψ1)(|\psi_1\rangle, |\psi_2\rangle) \mapsto (|\psi_2\rangle, |\psi_1\rangle). \square

Corollary 2.2. The physical two-fermion state lies in the antisymmetric subspace 2HHH\bigwedge^2 \mathcal{H} \subset \mathcal{H} \otimes \mathcal{H}.

Proof. The antisymmetric subspace is the (1)(-1)-eigenspace of P12P_{12}:

2H={ΨHH:P12Ψ=Ψ}\bigwedge^2 \mathcal{H} = \{|\Psi\rangle \in \mathcal{H} \otimes \mathcal{H} : P_{12}|\Psi\rangle = -|\Psi\rangle\}

Proposition 2.1 requires that the two-fermion state Ψ12|\Psi_{12}\rangle satisfies P12Ψ12=Ψ12P_{12}|\Psi_{12}\rangle = -|\Psi_{12}\rangle, which is precisely the membership condition for 2H\bigwedge^2 \mathcal{H}. \square

Step 3: Same-State Exchange Is the Identity

Proposition 3.1. If ψ1=ψ2=ψ|\psi_1\rangle = |\psi_2\rangle = |\psi\rangle, the exchange operator acts as the identity on the two-particle state.

Proof. This is immediate from the definition of P12P_{12}:

P12(ψψ)=ψψP_{12}(|\psi\rangle \otimes |\psi\rangle) = |\psi\rangle \otimes |\psi\rangle

The swap of two identical copies is the identity map. This is a purely algebraic statement about tensor products — it requires no physical assumptions. \square

Remark. This step does not assume a “preferred basis.” For any ψH|\psi\rangle \in \mathcal{H}, the product state ψψ|\psi\rangle \otimes |\psi\rangle is invariant under exchange by definition of the tensor product. The argument holds in any basis.

Step 4: The Exclusion Theorem

Theorem 4.1 (Pauli Exclusion). No nonzero antisymmetric state exists in which both fermions occupy the same single-particle state.

Proof. Suppose for contradiction that Ψ2H|\Psi\rangle \in \bigwedge^2 \mathcal{H} has both particles in state ψ|\psi\rangle. Then Ψ=cψψ|\Psi\rangle = c \cdot |\psi\rangle \otimes |\psi\rangle for some c0c \neq 0.

By Corollary 2.2 (antisymmetry):

P12Ψ=ΨP_{12}|\Psi\rangle = -|\Psi\rangle

By Proposition 3.1 (same-state identity):

P12Ψ=P12(cψψ)=cψψ=ΨP_{12}|\Psi\rangle = P_{12}(c \cdot |\psi\rangle \otimes |\psi\rangle) = c \cdot |\psi\rangle \otimes |\psi\rangle = |\Psi\rangle

Therefore Ψ=Ψ|\Psi\rangle = -|\Psi\rangle, which implies 2Ψ=02|\Psi\rangle = 0, hence Ψ=0|\Psi\rangle = 0.

This contradicts c0c \neq 0. Therefore no such state exists. \square

Corollary 4.2. The antisymmetric two-fermion state for states ψ,ϕ|\psi\rangle, |\phi\rangle is unique up to normalization:

Ψ12=12(ψϕϕψ)|\Psi_{12}\rangle = \frac{1}{\sqrt{2}}\left(|\psi\rangle \otimes |\phi\rangle - |\phi\rangle \otimes |\psi\rangle\right)

This vanishes identically when ϕ=ψ|\phi\rangle = |\psi\rangle.

Proof. The general element of 2H\bigwedge^2 \mathcal{H} built from ψ|\psi\rangle and ϕ|\phi\rangle is ψϕ=ψϕϕψ|\psi\rangle \wedge |\phi\rangle = |\psi\rangle \otimes |\phi\rangle - |\phi\rangle \otimes |\psi\rangle. Setting ϕ=ψ|\phi\rangle = |\psi\rangle gives ψψψψ=0|\psi\rangle \otimes |\psi\rangle - |\psi\rangle \otimes |\psi\rangle = 0. \square

Step 5: Generalization to NN Fermions

Theorem 5.1. For NN identical fermions with single-particle Hilbert space H\mathcal{H} of dimension dimH=d\dim \mathcal{H} = d, the NN-particle state lies in NH\bigwedge^N \mathcal{H}, which has dimension (dN)\binom{d}{N}. In particular:

Proof. The antisymmetric NN-fold tensor product NH\bigwedge^N \mathcal{H} has dimension (dN)\binom{d}{N}, which equals zero when N>dN > d (by convention, (dN)=0\binom{d}{N} = 0 for N>dN > d). This is because an antisymmetric tensor on NN vectors from a dd-dimensional space vanishes identically when N>dN > d — the vectors cannot all be linearly independent, and antisymmetry forces the tensor to vanish when any two inputs coincide. \square

Corollary 5.2 (Atomic shell structure). Electrons have H=L2(R3)C2\mathcal{H} = L^2(\mathbb{R}^3) \otimes \mathbb{C}^2 (position ×\times spin). For a hydrogen-like atom with principal quantum number nn, the number of available states at level nn is 2n22n^2 (factor of 2 from spin-1/2). The exclusion principle forces electrons into successively higher levels, producing the shell structure 1s22s22p63s21s^2 \, 2s^2 \, 2p^6 \, 3s^2 \, \ldots of the periodic table.

Step 6: Connection to Degeneracy Pressure

Proposition 6.1. The exclusion principle generates a quantum pressure (degeneracy pressure) that resists compression of fermionic matter. This pressure is geometric — it is the vanishing of the antisymmetric state space, not a dynamical force.

Proof. Consider NN identical fermions confined to a volume VV with density n=N/Vn = N/V. The available single-particle states in VV are plane waves with momenta p\mathbf{p} at discrete values set by the boundary conditions, with spacing Δp/V1/3\Delta p \sim \hbar/V^{1/3} in each direction (standard quantum mechanics in a box).

By Theorem 4.1, each state accommodates at most one fermion per spin component. At zero temperature, fermions fill states from lowest energy upward until all NN particles are placed. The highest occupied momentum is the Fermi momentum pFp_F, determined by the phase-space counting:

N=gsV(2π)34πpF33N = g_s \cdot \frac{V}{(2\pi\hbar)^3} \cdot \frac{4\pi p_F^3}{3}

where gs=2s+1g_s = 2s+1 is the spin degeneracy (gs=2g_s = 2 for spin-1/2). Solving: pF=(6π2n/gs)1/3n1/3p_F = \hbar(6\pi^2 n/g_s)^{1/3} \propto n^{1/3}.

The total kinetic energy is E=gsV(2π)30pFp22m4πp2dp=35NpF22mNn2/3E = g_s \cdot \frac{V}{(2\pi\hbar)^3} \int_0^{p_F} \frac{p^2}{2m} \cdot 4\pi p^2 dp = \frac{3}{5}N \frac{p_F^2}{2m} \propto N \cdot n^{2/3}. The degeneracy pressure is:

Pdeg=EVN=2E3V=(6π2)2/325mgs2/3n5/3P_{\text{deg}} = -\frac{\partial E}{\partial V}\bigg|_N = \frac{2E}{3V} = \frac{(6\pi^2)^{2/3}\hbar^2}{5m g_s^{2/3}} n^{5/3}

This pressure diverges as V0V \to 0 (nn \to \infty), preventing complete collapse — a geometric consequence of the vanishing of NH\bigwedge^N \mathcal{H} when more fermions are added than available states. In white dwarfs, electron degeneracy pressure supports the star against gravity (MCh1.4MM_{\text{Ch}} \approx 1.4 M_\odot, Chandrasekhar 1931). In neutron stars, neutron degeneracy pressure plays the same role. \square

Step 7: Bosonic Contrast

Proposition 7.1. For identical bosons (integer winding class [0][0]), the relational invariant is symmetric: I12(ψ1,ψ2)=I12(ψ2,ψ1)I_{12}(|\psi_1\rangle, |\psi_2\rangle) = I_{12}(|\psi_2\rangle, |\psi_1\rangle). No exclusion applies — arbitrarily many identical bosons can occupy the same state.

Proof. The symmetric subspace Sym2(H)HH\text{Sym}^2(\mathcal{H}) \subset \mathcal{H} \otimes \mathcal{H} contains the state ψψ|\psi\rangle \otimes |\psi\rangle for any ψ|\psi\rangle. The exchange operator acts as P12(ψψ)=ψψ=+1(ψψ)P_{12}(|\psi\rangle \otimes |\psi\rangle) = |\psi\rangle \otimes |\psi\rangle = +1 \cdot (|\psi\rangle \otimes |\psi\rangle), consistent with the symmetric requirement. No contradiction arises. This is the basis for Bose-Einstein condensation — macroscopic occupation of a single quantum state. \square

Remark (Species decomposition and partial exclusion). The Pauli exclusion principle applies only to identical fermions — those sharing the same winding class [γ]π1(Q)[\gamma] \in \pi_1(Q) (same species). Non-identical fermions (e.g., electron and muon) belong to different winding classes and have independent loop structures. Formally: the multi-observer state space decomposes as H=αHα\mathcal{H} = \bigotimes_\alpha \mathcal{H}_\alpha where α\alpha indexes distinct winding classes (species). The antisymmetrization requirement (from π1=Z2\pi_1 = \mathbb{Z}_2) applies within each sector Hα\mathcal{H}_\alpha, not between sectors. An electron and a muon can occupy the same spatial state because they reside in different sectors — their winding numbers are independently defined. This is exactly the standard physics: Pauli exclusion applies per species, and species labels are the framework’s winding class labels. No additional axiom is needed; the sector decomposition is a direct consequence of the topological classification of loop types.

Comparison with Standard Physics

AspectStandard QMObserver-centrism
Pauli exclusionPostulated (or derived from QFT)Derived from π1(SO(3))=Z2\pi_1(SO(3)) = \mathbb{Z}_2 + algebra
AntisymmetryPostulated for fermionsTopological: winding class [1][1]
Why ψ=0\psi = 0 for same state"x=x    x=0x = -x \implies x = 0"Same algebraic identity, but the antisymmetry itself is derived
Degeneracy pressureKinetic energy + exclusionGeometric: vanishing of NH\bigwedge^N \mathcal{H}
Bose-Einstein condensationSymmetric wavefunctionsWinding class [0][0] permits same-state occupation

Consistency Model

Theorem 8.1. The helium atom provides a consistency model for the Pauli exclusion principle.

Verification. Take two electrons (s=1/2s = 1/2, fermions) in the helium atom with H=L2(R3)C2\mathcal{H} = L^2(\mathbb{R}^3) \otimes \mathbb{C}^2.

Rigor Assessment

Fully rigorous:

Rigorous given spin-statistics:

Upstream dependency:

Assessment: The Pauli exclusion principle is rigorous. The core theorem (Theorem 4.1) is a pure algebraic identity: antisymmetry + same state → zero. The antisymmetry itself is rigorous (from the spin-statistics connection, now upgraded to rigorous). The physical consequences — shell structure, degeneracy pressure, stability of matter — are standard results following from the algebraic structure.

Open Gaps

  1. Fermi-Dirac statistics: The full Fermi-Dirac distribution nk=1/(e(ϵkμ)/kBT+1)\langle n_k \rangle = 1/(e^{(\epsilon_k - \mu)/k_BT} + 1) should be derivable from the exclusion principle (each state occupied by 0 or 1 fermion) plus the entropy framework (Entropy).
  2. Stability of matter: Lieb and Thirring (1975) proved that the stability of ordinary matter (energy extensive in particle number) requires the Pauli exclusion principle. This should be connected to the framework’s structural explanation of matter stability.

Addressed Gaps

  1. Partial exclusionResolved: The species concept is formalized via the winding class decomposition H=αHα\mathcal{H} = \bigotimes_\alpha \mathcal{H}_\alpha, where α\alpha indexes distinct winding classes [γ]π1(Q)[\gamma] \in \pi_1(Q). Antisymmetrization applies within each sector, not between sectors. See Remark after Step 7.