jain_denominator_odd_minus

formal source

 107  linarith [show (2 * m * p + 1) % 2 = (2 * (m * p) + 1) % 2 from by ring_nf]
 108
 109/-- The denominator of a Jain fraction is odd (for ν = p/(2mp-1) when 2mp > 1). -/
 110theorem jain_denominator_odd_minus (p m : ℕ) (h : 1 < 2 * m * p) :
 111    (2 * m * p - 1) % 2 = 1 := by
 112  have hk : 2 * m * p = 2 * (m * p) := by ring
 113  have hkge : 1 < 2 * (m * p) := by linarith [hk]
 114  have : (2 * (m * p) - 1) % 2 = 1 := by omega
 115  linarith [show (2 * m * p - 1) % 2 = (2 * (m * p) - 1) % 2 from by ring_nf]
 116
 117/-- **KEY THEOREM**: FQHE requires odd denominator. -/
 118theorem fqhe_odd_denominator (p m : ℕ) (hp : 0 < p) (hm : 0 < m) :
 119    ¬ (2 * m * p + 1) % 2 = 0 := by
 120  have := jain_denominator_odd_plus p m hp hm
 121  omega
 122
 123/-- The ν = 1/3 Laughlin state is in the Jain sequence (m=1, p=1, plus). -/
 124theorem one_third_in_jain_sequence :
 125    jain_fraction 1 1 true = 1/3 := by
 126  unfold jain_fraction
 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. -/