ExchangeSymmetry
plain-language theorem explainer
ExchangeSymmetry classifies wavefunctions as symmetric or antisymmetric under particle exchange. Physicists deriving spin-statistics relations from discrete time structures cite it to link spin parity to exchange sign. The declaration is a direct inductive definition with two constructors that follows from the 8-tick phase cycle.
Claim. The exchange symmetry type for a wavefunction is either symmetric, where the wavefunction satisfies $ψ(1,2) = +ψ(2,1)$, or antisymmetric, where it satisfies $ψ(1,2) = -ψ(2,1)$.
background
The QFT module derives the spin-statistics connection from the 8-tick cycle in which a 2π rotation traverses eight discrete ticks. Half-integer spin particles require two full cycles (16 ticks) to return to the identity state and therefore accumulate a phase factor of -1, while integer spin particles require one cycle and accumulate +1. This setting rests on the upstream result from PrimitiveDistinction, which reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
The declaration is an inductive definition that introduces the two constructors symmetric and antisymmetric with no further proof obligations.
why it matters
It supplies the symmetry classification used by exchangeSymmetryFromSpin, fermion_antisymmetric_wavefunction, boson_symmetric_wavefunction, and the SpinStatisticsFalsifier structure. The definition fills the QFT-001 target of obtaining the spin-statistics theorem from the 8-tick phase mechanism and directly implements the eight-tick octave landmark (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.