fermion_wavefunction_antisymmetric
plain-language theorem explainer
The declaration establishes that half-integer spin yields antisymmetric exchange symmetry for wavefunctions. Researchers deriving Pauli exclusion from Recognition Science ledger single-occupancy would cite it to link spin to state occupancy constraints. The proof is a one-line wrapper that specializes the general fermion antisymmetry theorem to Spin.half and confirms the half-integer predicate by decision.
Claim. For half-integer spin $s = 1/2$, the exchange symmetry is antisymmetric: the wavefunction satisfies $ψ(1,2) = -ψ(2,1)$.
background
ExchangeSymmetry is an inductive type with constructors symmetric (wavefunction unchanged under exchange) and antisymmetric (wavefunction changes sign). The function exchangeSymmetryFromSpin maps Spin to this type, returning antisymmetric exactly when the spin is half-integer. The upstream theorem fermion_antisymmetric_wavefunction states that any half-integer spin satisfies this mapping. In the QFT.PauliExclusion module the result supports derivation of the Pauli exclusion principle from ledger single-occupancy, where fermions are odd-phase entries in the eight-tick cycle that force ψ(a,a) = 0.
proof idea
The proof applies the general theorem fermion_antisymmetric_wavefunction to the concrete value Spin.half, then uses decide to discharge the isHalfInteger hypothesis.
why it matters
This theorem supplies the spin-statistics link required for the module's target derivation of atomic shell structure and the periodic table. It sits inside the Recognition Science chain that obtains fermions from the eight-tick octave (T7) and odd-phase ledger entries, feeding the broader Pauli exclusion argument that yields degeneracy pressure and matter stability. The module doc-comment flags the intended PRB paper on first-principles atomic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.