iqhe_filling
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not encode the physical constants e or h that appear in the conductance formula.
- Does not treat fractional filling factors or composite-fermion states.
- Does not derive the Chern number from the eight-tick ledger; that step is handled elsewhere.
- Does not specify the magnetic-field or density conditions under which n levels are filled.
formal statement (Lean)
60def iqhe_filling (n : ℕ) : ℚ := n
proof body
Definition body.
61
62/-- For IQHE: σ_xy = ν × e²/h with ν ∈ ℤ. -/