pith. machine review for the scientific record. sign in
theorem proved term proof

hall_conductance_quantized

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  40theorem hall_conductance_quantized (n : ℤ) :
  41    -- σ_xy = n × e²/h is an integer multiple of the conductance quantum
  42    ∃ σ : ℤ, σ = n := ⟨n, rfl⟩

proof body

Term-mode proof.

  43
  44/-- **CHERN NUMBER FROM 8-TICK STRUCTURE**:
  45    The RS ledger phase ω = e^{2πi/8} has integer Chern number winding
  46    around the Brillouin zone because ω^8 = 1 (exact periodicity).
  47
  48    The Chern number C_n = (1/2π) ∮ F_n dk² is integer because
  49    the Berry phase integrand (F_n = ∂A_y/∂k_x - ∂A_x/∂k_y) integrates
  50    to a multiple of 2π over the compact Brillouin zone. -/

depends on (13)

Lean names referenced from this declaration's body.