`PhaseEntry`

definition

show as: view math explainer →

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

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

formal source

 230/-! ## Connection to 8-Tick Ledger -/
 231
 232/-- A ledger entry type for tracking phase. -/
 233structure PhaseEntry where
 234  /-- The accumulated phase. -/
 235  phase : ℂ
 236  /-- Number of ticks elapsed. -/
 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

papers checked against this theorem

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