two_fifth_in_jain_sequence

formal source

 127  norm_num
 128
 129/-- The ν = 2/5 state is in the Jain sequence (m=1, p=2, plus). -/
 130theorem two_fifth_in_jain_sequence :
 131    jain_fraction 2 1 true = 2/5 := by
 132  unfold jain_fraction
 133  norm_num
 134
 135/-! ## Laughlin Quasi-particle Charge -/
 136
 137/-- At filling ν = 1/q, quasi-particles carry fractional charge e/q. -/
 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 : ℕ) : ℝ :=