`laughlin_exchange_phase`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.QuantumHallEffect
domain: Physics
line: 160 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.QuantumHallEffect on GitHub at line 160.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 157    with exchange phase θ = π/q.
 158    For q = 1 (electrons): θ = π → fermions. ✓
 159    For q = 3 (ν=1/3 quasi-holes): θ = π/3 → anyons. -/
 160noncomputable def laughlin_exchange_phase (q : ℕ) : ℝ :=
 161  Real.pi / q
 162
 163/-- Electron exchange phase = π (fermion). -/
 164theorem electron_exchange_phase : laughlin_exchange_phase 1 = Real.pi := by
 165  unfold laughlin_exchange_phase
 166  simp
 167
 168/-- ν = 1/3 quasi-particle exchange phase = π/3. -/
 169theorem one_third_exchange_phase :
 170    laughlin_exchange_phase 3 = Real.pi / 3 := by
 171  unfold laughlin_exchange_phase
 172  norm_num
 173
 174end QHE
 175end Physics
 176end IndisputableMonolith

papers checked against this theorem

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