iqhe_conductance_integer

formal source

  60def iqhe_filling (n : ℕ) : ℚ := n
  61
  62/-- For IQHE: σ_xy = ν × e²/h with ν ∈ ℤ. -/
  63theorem iqhe_conductance_integer (n : ℕ) :
  64    ∃ σ : ℕ, σ = n := ⟨n, rfl⟩
  65
  66/-- The von Klitzing constant R_K = h/e² is the resistance quantum. -/
  67-- R_K ≈ 25812.807 Ω (exact in the 2019 SI revision)
  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