antisymmetry_implies_exclusion
plain-language theorem explainer
Antisymmetry of a fermion wavefunction ψ(a,b) = −ψ(b,a) forces the diagonal entries ψ(a,a) to vanish, which encodes that no two identical fermions can occupy the same quantum state. Atomic and condensed-matter physicists cite this when deriving shell structure from ledger single-occupancy. The proof is a one-line wrapper that applies the core antisymmetry lemma pauli_core.
Claim. Let $ψ : ℕ → ℕ → ℂ$ be a complex-valued function on pairs of natural numbers. If $ψ(a,b) = −ψ(b,a)$ holds for all $a,b ∈ ℕ$, then $ψ(a,a) = 0$ for every $a$.
background
In Recognition Science the Pauli exclusion principle follows from ledger single-occupancy. Fermions are odd-phase ledger entries under the eight-tick cycle, so their two-particle wavefunctions must satisfy antisymmetry to keep the ledger balanced. The module QFT-004 derives this directly from the Recognition Composition Law and the forcing chain T0–T8.
proof idea
The proof is a one-line wrapper that applies pauli_core to the supplied antisymmetry hypothesis.
why it matters
This theorem supplies the mathematical step from antisymmetry to exclusion and feeds the sibling results on subshell and shell capacities. It realizes the spin-statistics link for half-integer spin (T5 J-uniqueness and T7 eight-tick octave) and supports the paper proposition on first-principles derivation of atomic shell structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.