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.
pauli_exclusion_core
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:
- From the spin-statistics derivation, identical fermions (particles with half-integer spin) have wavefunctions that pick up a minus sign when two particles are exchanged.
- If two fermions are in the same state, swapping them changes nothing — the state is identical before and after.
- But antisymmetry demands a minus sign. A quantity that equals both itself and its own negative must be zero.
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 is antisymmetric under exchange and the exchange is trivial (same state), then — the configuration is coherence-forbidden.
Derivation
Step 1: Setup and Definitions
Definition 1.1. Let be the single-particle Hilbert space of states for a fermion species. A two-fermion state is a vector in . The exchange operator is the linear map defined by .
Definition 1.2. The relational invariant of two identical observers in states is a function on encoding the joint coherence structure of the pair. Physically, is the outcome of a Type III interaction between and (from Relational Invariants).
Step 2: Antisymmetry from Spin-Statistics
Proposition 2.1. For identical fermions (half-integer winding class ), the relational invariant is antisymmetric under exchange:
Proof. This is Proposition 4.1 of Spin and Statistics. The exchange phase for winding class is . The relational invariant, as a function on , inherits this phase under the swap .
Corollary 2.2. The physical two-fermion state lies in the antisymmetric subspace .
Proof. The antisymmetric subspace is the -eigenspace of :
Proposition 2.1 requires that the two-fermion state satisfies , which is precisely the membership condition for .
Step 3: Same-State Exchange Is the Identity
Proposition 3.1. If , the exchange operator acts as the identity on the two-particle state.
Proof. This is immediate from the definition of :
The swap of two identical copies is the identity map. This is a purely algebraic statement about tensor products — it requires no physical assumptions.
Remark. This step does not assume a “preferred basis.” For any , the product state 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 has both particles in state . Then for some .
By Corollary 2.2 (antisymmetry):
By Proposition 3.1 (same-state identity):
Therefore , which implies , hence .
This contradicts . Therefore no such state exists.
Corollary 4.2. The antisymmetric two-fermion state for states is unique up to normalization:
This vanishes identically when .
Proof. The general element of built from and is . Setting gives .
Step 5: Generalization to Fermions
Theorem 5.1. For identical fermions with single-particle Hilbert space of dimension , the -particle state lies in , which has dimension . In particular:
- If , then — no valid state exists.
- At most identical fermions can coexist.
Proof. The antisymmetric -fold tensor product has dimension , which equals zero when (by convention, for ). This is because an antisymmetric tensor on vectors from a -dimensional space vanishes identically when — the vectors cannot all be linearly independent, and antisymmetry forces the tensor to vanish when any two inputs coincide.
Corollary 5.2 (Atomic shell structure). Electrons have (position spin). For a hydrogen-like atom with principal quantum number , the number of available states at level is (factor of 2 from spin-1/2). The exclusion principle forces electrons into successively higher levels, producing the shell structure 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 identical fermions confined to a volume with density . The available single-particle states in are plane waves with momenta at discrete values set by the boundary conditions, with spacing 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 particles are placed. The highest occupied momentum is the Fermi momentum , determined by the phase-space counting:
where is the spin degeneracy ( for spin-1/2). Solving: .
The total kinetic energy is . The degeneracy pressure is:
This pressure diverges as (), preventing complete collapse — a geometric consequence of the vanishing of when more fermions are added than available states. In white dwarfs, electron degeneracy pressure supports the star against gravity (, Chandrasekhar 1931). In neutron stars, neutron degeneracy pressure plays the same role.
Step 7: Bosonic Contrast
Proposition 7.1. For identical bosons (integer winding class ), the relational invariant is symmetric: . No exclusion applies — arbitrarily many identical bosons can occupy the same state.
Proof. The symmetric subspace contains the state for any . The exchange operator acts as , consistent with the symmetric requirement. No contradiction arises. This is the basis for Bose-Einstein condensation — macroscopic occupation of a single quantum state.
Remark (Species decomposition and partial exclusion). The Pauli exclusion principle applies only to identical fermions — those sharing the same winding class (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 where indexes distinct winding classes (species). The antisymmetrization requirement (from ) applies within each sector , 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
| Aspect | Standard QM | Observer-centrism |
|---|---|---|
| Pauli exclusion | Postulated (or derived from QFT) | Derived from + algebra |
| Antisymmetry | Postulated for fermions | Topological: winding class |
| Why for same state | "" | Same algebraic identity, but the antisymmetry itself is derived |
| Degeneracy pressure | Kinetic energy + exclusion | Geometric: vanishing of |
| Bose-Einstein condensation | Symmetric wavefunctions | Winding class 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 (, fermions) in the helium atom with .
- Antisymmetry (Corollary 2.2): The ground-state wavefunction is antisymmetric under exchange: .
- Exclusion (Theorem 4.1): Both electrons in with same spin would give , which is symmetric — forbidden.
- Ground state: The configuration has spatial wavefunction (symmetric) times spin singlet (antisymmetric). Product is antisymmetric.
- Shell structure (Corollary 5.2): The shell accommodates exactly 2 electrons (, ). A third electron must go to — beginning lithium.
- Degeneracy pressure (Proposition 6.1): White dwarf Sirius B has , — supported by electron degeneracy pressure against gravitational collapse.
Rigor Assessment
Fully rigorous:
- Theorem 4.1: The exclusion argument () is a tautology of linear algebra — the core of the derivation
- Corollary 4.2: Antisymmetrized product vanishing at coincidence (standard exterior algebra)
- Theorem 5.1: (standard multilinear algebra)
- Proposition 6.1: Degeneracy pressure from Fermi momentum counting (standard quantum statistical mechanics)
- Proposition 7.1: Bosonic non-exclusion (symmetric counterpart)
- Theorem 8.1: Consistency model verified on helium atom
Rigorous given spin-statistics:
- Proposition 2.1, Corollary 2.2: Antisymmetry of fermionic states follows from Spin and Statistics (Theorem 3.3 + Proposition 4.1), which is now rigorous.
Upstream dependency:
- The identification of abstract relational invariants with quantum-mechanical wavefunctions uses the amplitude–coherence identification (S1 of Born Rule). Given this identification, the exclusion principle follows with mathematical certainty.
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
- Fermi-Dirac statistics: The full Fermi-Dirac distribution should be derivable from the exclusion principle (each state occupied by 0 or 1 fermion) plus the entropy framework (Entropy).
- 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
- Partial exclusion — Resolved: The species concept is formalized via the winding class decomposition , where indexes distinct winding classes . Antisymmetrization applies within each sector, not between sectors. See Remark after Step 7.