laughlin_charge_one_third

formal source

 138def laughlin_quasi_charge (q : ℕ) : ℚ := 1 / q
 139
 140/-- At ν = 1/3: quasi-particle charge = e/3. -/
 141theorem laughlin_charge_one_third :
 142    laughlin_quasi_charge 3 = 1/3 := by
 143  simp [laughlin_quasi_charge]
 144
 145/-- Quasi-particle charge is smaller for larger q. -/
 146theorem quasi_charge_decreasing (q₁ q₂ : ℕ) (h1 : 0 < q₁) (h2 : 0 < q₂) (h : q₁ < q₂) :
 147    laughlin_quasi_charge q₂ < laughlin_quasi_charge q₁ := by
 148  unfold laughlin_quasi_charge
 149  have hq1 : (0 : ℚ) < q₁ := by exact_mod_cast h1
 150  have hq2 : (0 : ℚ) < q₂ := by exact_mod_cast h2
 151  have hlt : (q₁ : ℚ) < q₂ := by exact_mod_cast h
 152  exact div_lt_div_of_pos_left one_pos hq1 hlt
 153
 154/-! ## Exchange Statistics in FQHE -/
 155
 156/-- **ANYONIC STATISTICS**: Laughlin quasi-particles at ν = 1/q are anyons
 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