iqhe_filling
plain-language theorem explainer
The declaration defines the integer quantum Hall filling factor as the rational number equal to the count of filled Landau levels. Condensed-matter theorists deriving quantized Hall conductance from topological invariants would reference it when stating σ_xy = ν e²/h for integer ν. The implementation is a one-line identity that maps each natural number directly to the corresponding rational.
Claim. The integer quantum Hall filling factor is defined by $ν(n) = n$ for each natural number $n$, representing the number of occupied Landau levels.
background
The module treats the quantum Hall effect as a consequence of the RS topological ledger. The integer case (IQHE) occurs when an integer number of Landau levels are filled, making the Hall conductance σ_xy = n e²/h a topological invariant equal to the Chern number. This rests on the eight-tick phase structure imported from EightTick and the J-cost framework that supplies the underlying balance condition.
proof idea
Direct definition that returns the input natural number cast to a rational; no lemmas or tactics are applied.
why it matters
This supplies the integer filling factor required by the quantized Hall conductance result listed in the module. It anchors the IQHE case inside the eight-tick octave that forces the Chern number to be integer, as described in the module's key results and the paper RS_Quantum_Hall_Effect.tex. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.