exchangeSymmetryFromSpin
plain-language theorem explainer
The definition maps each spin quantum number to its exchange symmetry under particle interchange. Researchers deriving spin-statistics relations from discrete phase cycles would cite this to link half-integer spins with antisymmetric wavefunctions. It is realized as a direct conditional branch on the isHalfInteger predicate.
Claim. For spin quantum number $s$, the exchange symmetry is antisymmetric when $s$ is half-integer and symmetric otherwise.
background
Spin is the structure holding twice the spin value as an integer together with a non-negativity proof. ExchangeSymmetry is the inductive type with constructors symmetric (wavefunction unchanged under swap) and antisymmetric (wavefunction negated under swap). The module sets the local context as derivation of the spin-statistics theorem from the 8-tick cycle: a $2π$ rotation traverses one full cycle, half-integer spins require two cycles for identity and therefore accumulate a minus sign.
proof idea
One-line definition that inspects the isHalfInteger predicate on the input spin and returns the matching ExchangeSymmetry constructor.
why it matters
It supplies the central mapping used by fermion_antisymmetric_wavefunction and boson_symmetric_wavefunction, which in turn feed PauliExclusion.fermion_wavefunction_antisymmetric. The declaration realizes the QFT-001 target of obtaining spin-statistics from 8-tick phase accumulation, directly instantiating the eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.