boson_symmetric_wavefunction
plain-language theorem explainer
Bosons, defined via integer spin, possess symmetric wavefunctions under exchange. Recognition Science derives this from phase accumulation over the eight-tick cycle, where integer spin yields a +1 factor. Researchers working on discrete-time foundations of QFT would cite the result. The proof unfolds the exchange symmetry definition and obtains a contradiction via mutual exclusivity of integer and half-integer spin.
Claim. Let $s$ be a spin quantum number. If $s$ is an integer, then the exchange symmetry of the associated wavefunction is symmetric.
background
The Spin structure encodes half-integer values by storing twice the spin as a nonnegative integer. ExchangeSymmetry is the inductive type with constructors symmetric and antisymmetric. The definition exchangeSymmetryFromSpin returns antisymmetric precisely when the spin is half-integer and symmetric otherwise, implementing the phase rule exp(2πi s) from the eight-tick cycle described in the module.
proof idea
The term proof first simplifies with the definition of exchangeSymmetryFromSpin. It then introduces the assumption that the spin is half-integer and applies the int_half_exclusive lemma to derive a contradiction with the supplied integer hypothesis.
why it matters
The declaration supplies the bosonic half of the spin-statistics connection inside the eight-tick phase framework (T7). It directly supports the subsequent Pauli exclusion argument in the same module and fills the integer-spin case of the paper proposition deriving statistics from discrete time structure rather than Lorentz invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.