 237  ticks : ℕ
 238
 239/-- Phase accumulated per tick for spin s. -/
 240noncomputable def phasePerTick (s : Spin) : ℂ :=
 241  Complex.exp (2 * π * I * s.value / 8)
 242
 243/-- **THEOREM**: 8 ticks gives the full cycle phase. -/
 244theorem eight_ticks_full_cycle (s : Spin) :
 245    (phasePerTick s) ^ 8 = cyclePhase s := by
 246  unfold phasePerTick cyclePhase
 247  rw [← Complex.exp_nat_mul]
 248  congr 1
 249  ring
 250
 251/-! ## Examples: Standard Model Particles -/
 252
 253/-- Electron has spin 1/2 (fermion). -/
 254example : Spin.half.isHalfInteger := by decide
 255
 256/-- Photon has spin 1 (boson). -/
 257example : Spin.one.isInteger := by decide
 258
 259/-- Electron obeys Fermi-Dirac statistics. -/
 260example : statisticsFromSpin Spin.half = Statistics.fermiDirac := by
 261  apply spin_statistics_fermion
 262  decide
 263
 264/-- Photon obeys Bose-Einstein statistics. -/
 265example : statisticsFromSpin Spin.one = Statistics.boseEinstein := by
 266  apply spin_statistics_boson
 267  decide
 268
 269/-! ## Falsification Criteria -/
 270

papers checked against this theorem

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