`boson_symmetric`

proved

show as: view math explainer →

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

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

 141
 142/-- **THEOREM (Boson Phase)**: Integer spin particles acquire +1
 143    under the full 8-tick cycle (2π rotation). -/
 144theorem boson_symmetric (s : Spin) (h : s.isInteger) :
 145    cyclePhase s = 1 := by
 146  unfold cyclePhase Spin.value Spin.isInteger at *
 147  -- s.twice is even, so s.twice % 2 = 0
 148  have heven : s.twice % 2 = 0 := h
 149  -- Get k such that s.twice = 2k
 150  have ⟨k, hk⟩ := Int.even_iff.mpr heven
 151  -- The phase is exp(2πi × (twice/2)) = exp(2πi × k) = 1
 152  have h_rewrite : 2 * π * I * (s.twice / 2 : ℝ) = (k : ℂ) * (2 * π * I) := by
 153    rw [hk]
 154    push_cast
 155    ring
 156  rw [h_rewrite, Complex.exp_int_mul_two_pi_mul_I]
 157
 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

papers checked against this theorem

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