`statisticsFromSpin`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.SpinStatistics on GitHub at line 167.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.