landau_energy
plain-language theorem explainer
Landau energy levels follow E_n = ω_c (n + 1/2) in the RS treatment of quantum Hall physics. Modelers of the integer quantum Hall effect cite this for the zero-point shift tied to fermionic phase. It is introduced as a direct definition without further lemmas.
Claim. The energy of the nth Landau level at cyclotron frequency ω_c is E_n = ω_c (n + 1/2).
background
The Quantum Hall Effect module derives the integer quantized Hall conductance from the topological Chern number of occupied Landau levels, with the fractional case arising from composite fermions under 8-tick balance. Landau levels are introduced with the standard energy formula, where the half-integer offset is interpreted as the zero-point energy from the 4-tick fermionic phase in the eight-tick octave structure. This connects to the foundation's T7 eight-tick period and the J-cost framework imported in the module.
proof idea
The declaration is a one-line definition assigning the value ω_c multiplied by (n plus one half).
why it matters
It provides the energy expression required by the downstream theorems landau_spacing, which establishes equal level spacing of ω_c, and zero_point_energy, which isolates the fermionic zero-point term. The definition supports the derivation of quantized Hall conductance σ_xy = n e²/h from the Chern number integer, consistent with the eight-tick phase topology in the RS framework. It touches the open question of how the 4-tick phase enforces the odd-denominator rule in Jain fractions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.