`electron_exchange_phase`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.QuantumHallEffect on GitHub at line 164.

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

 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.