hall_conductance_quantized
plain-language theorem explainer
The Hall conductance in units of e²/h equals the Chern number for any integer n. Condensed matter physicists modeling topological invariants in the integer quantum Hall effect cite this to confirm quantization. The proof is a one-line term construction that directly witnesses the existential with the input n and applies reflexivity.
Claim. The Hall conductance satisfies $σ_{xy} = n e^2/h$ for integer $n ∈ ℤ$, where the conductance is an integer multiple of the quantum $e^2/h$ and equals the Chern number.
background
The module treats the integer quantum Hall effect as a topological invariant of Landau levels in the RS ledger. Hall conductance in units of e²/h is identified with the Chern number of occupied states. The 8-tick phase supplies discrete angles kπ/4 whose eighth power equals 1, forcing the Berry phase integral over the Brillouin zone to be an integer multiple of 2π. Upstream, the phase definition establishes exact periodicity with period 2π.
proof idea
The proof is a term-mode construction. It applies the existential introduction constructor to the parameter n and pairs it with reflexivity to establish equality of σ to n.
why it matters
This anchors integer quantization of Hall conductance to the Chern number arising from 8-tick topology. It supports the module's results on chern_number_integer, iqhe_conductance_integer, and jain_sequence. It fills the quantization step in RS_Quantum_Hall_Effect.tex. The eight-tick octave periodicity guarantees the integer winding number, consistent with T7 in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.