zero_point_energy

formal source

  86  ring
  87
  88/-- Zero-point energy is 1/2 ℏω_c — the fermionic half-period contribution. -/
  89theorem zero_point_energy (ω_c : ℝ) :
  90    landau_energy 0 ω_c = ω_c / 2 := by
  91  unfold landau_energy
  92  ring
  93
  94/-! ## FQHE - Fractional Quantum Hall Effect -/
  95
  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