landau_spacing
plain-language theorem explainer
Landau levels are equally spaced by the cyclotron frequency ω_c. Condensed matter physicists deriving quantized Hall conductance from topological invariants would cite this spacing when computing filling factors or density of states. The proof is a direct algebraic reduction obtained by unfolding the energy definition and applying ring simplification.
Claim. For any natural number $n$ and positive real number $ω_c > 0$, the Landau level energies satisfy $E_{n+1}(ω_c) - E_n(ω_c) = ω_c$, where $E_k(ω_c)$ denotes the energy of the $k$-th Landau level.
background
The module treats the integer quantum Hall effect as arising from the RS topological ledger with eight-tick periodicity. Landau levels are the single-particle states in a magnetic field whose energies incorporate a fermionic zero-point shift of 1/2 ω_c. The local setting states that the Hall conductance σ_xy = n e²/h is a Chern number invariant of the occupied levels, with the spacing result supplying the uniform ladder needed for integer filling.
proof idea
The term proof unfolds the definition of landau_energy, applies push_cast to align the natural-number indexing, and invokes ring to confirm the difference of consecutive terms equals ω_c.
why it matters
The spacing supplies the uniform energy ladder required by the module's integer quantum Hall results such as hall_conductance_quantized and chern_number_integer_from_8tick. It aligns with the eight-tick octave (T7) by guaranteeing equal increments consistent with the period-8 topological structure. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.