RK_positive

formal source

  68abbrev von_klitzing_constant : ℝ := 25812.807  -- Ohms
  69
  70/-- R_K is positive. -/
  71theorem RK_positive : 0 < von_klitzing_constant := by norm_num
  72
  73/-! ## Landau Levels -/
  74
  75/-- **LANDAU QUANTIZATION**: E_n = ℏω_c(n + 1/2)
  76    The factor 1/2 is the zero-point energy of spin-1/2 fermions.
  77    In RS: the 1/2 comes from the 4-tick (half-period) fermionic phase. -/
  78noncomputable def landau_energy (n : ℕ) (ω_c : ℝ) : ℝ :=
  79  ω_c * (n + 1/2)
  80
  81/-- Landau levels are equally spaced. -/
  82theorem landau_spacing (n : ℕ) (ω_c : ℝ) (hω : 0 < ω_c) :
  83    landau_energy (n+1) ω_c - landau_energy n ω_c = ω_c := by
  84  unfold landau_energy
  85  push_cast
  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