`statisticsFromSpin`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SpinStatistics
domain: QFT
line: 167 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 167.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 164deriving DecidableEq, Repr
 165
 166/-- Determine statistics from spin. -/
 167def statisticsFromSpin (s : Spin) : Statistics :=
 168  if s.isHalfInteger then Statistics.fermiDirac else Statistics.boseEinstein
 169
 170/-- **THEOREM (Spin-Statistics)**: Half-integer spin implies Fermi-Dirac statistics. -/
 171theorem spin_statistics_fermion (s : Spin) (h : s.isHalfInteger) :
 172    statisticsFromSpin s = Statistics.fermiDirac := by
 173  simp [statisticsFromSpin, h]
 174
 175/-- **THEOREM (Spin-Statistics)**: Integer spin implies Bose-Einstein statistics. -/
 176theorem spin_statistics_boson (s : Spin) (h : s.isInteger) :
 177    statisticsFromSpin s = Statistics.boseEinstein := by
 178  simp [statisticsFromSpin]
 179  intro h'
 180  exact absurd (And.intro h h') (Spin.int_half_exclusive s)
 181
 182/-! ## Exchange Symmetry -/
 183
 184/-- Symmetry type for wavefunction under particle exchange. -/
 185inductive ExchangeSymmetry where
 186  | symmetric     -- ψ(1,2) = +ψ(2,1)
 187  | antisymmetric -- ψ(1,2) = -ψ(2,1)
 188deriving DecidableEq, Repr
 189
 190/-- Determine exchange symmetry from spin. -/
 191def exchangeSymmetryFromSpin (s : Spin) : ExchangeSymmetry :=
 192  if s.isHalfInteger then ExchangeSymmetry.antisymmetric
 193  else ExchangeSymmetry.symmetric
 194
 195/-- **THEOREM**: Fermions have antisymmetric wavefunctions. -/
 196theorem fermion_antisymmetric_wavefunction (s : Spin) (h : s.isHalfInteger) :
 197    exchangeSymmetryFromSpin s = ExchangeSymmetry.antisymmetric := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.