jain_fraction

formal source

  96/-- The Jain sequence of allowed FQHE fractions:
  97    ν = p/(2mp ± 1) for positive integers p, m.
  98    The denominator must be ODD (from Fermi statistics). -/
  99def jain_fraction (p m : ℕ) (plus : Bool) : ℚ :=
 100  if plus then p / (2 * m * p + 1) else p / (2 * m * p - 1)
 101
 102/-- The denominator of a Jain fraction is odd (for ν = p/(2mp+1)). -/
 103theorem jain_denominator_odd_plus (p m : ℕ) (hp : 0 < p) (hm : 0 < m) :
 104    (2 * m * p + 1) % 2 = 1 := by
 105  have h : 2 * m * p = 2 * (m * p) := by ring
 106  have : (2 * (m * p) + 1) % 2 = 1 := by omega
 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). -/