`Statistics`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.SpinStatistics
domain: QFT
line: 161 · 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 161.

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

 158/-! ## Particle Statistics Classification -/
 159
 160/-- Particle statistics type. -/
 161inductive Statistics where
 162  | fermiDirac
 163  | boseEinstein
 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 :=

papers checked against this theorem

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