fermion_antisymmetric_wavefunction
plain-language theorem explainer
Half-integer spin particles have antisymmetric wavefunctions under exchange. Researchers connecting spin-statistics to discrete phase cycles in Recognition Science models would cite this result. The proof reduces directly by simplification of the exchange symmetry definition once the half-integer hypothesis is supplied.
Claim. Let $s$ be a spin quantum number. If $s$ satisfies the half-integer condition, then the exchange symmetry determined from $s$ equals the antisymmetric type.
background
The Spin structure encodes the quantum number via an integer twice the value, preserving exact arithmetic while enforcing non-negativity. ExchangeSymmetry is the inductive type with constructors symmetric and antisymmetric, capturing wavefunction sign change under particle exchange. The module derives the spin-statistics link from 8-tick phase accumulation: a $2π$ rotation traverses one full cycle, so half-integer spins require two cycles and acquire a minus sign.
proof idea
The term proof applies the simp tactic to the definition of exchangeSymmetryFromSpin together with the supplied half-integer hypothesis, which selects the antisymmetric branch by construction.
why it matters
This result is applied directly by fermion_wavefunction_antisymmetric in the PauliExclusion module to obtain the concrete case for spin 1/2. It completes one step of the QFT-001 derivation of spin-statistics from the eight-tick octave structure, supplying the fermion half of the connection that feeds Pauli exclusion bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.