iqhe_conductance_integer
plain-language theorem explainer
The declaration asserts that the integer quantum Hall conductance takes any prescribed natural number value n. Condensed matter physicists working on topological invariants in the quantum Hall regime would cite this when connecting the Chern number to the filling factor ν. The proof is a direct term-mode construction that supplies the witness n and closes the equality by reflexivity.
Claim. For any natural number $n$, there exists a natural number $σ$ such that $σ = n$. In the IQHE setting this encodes the statement that the Hall conductance $σ_{xy}$ equals the integer filling factor $ν ∈ ℤ$ (i.e., $σ_{xy} = ν e^2/h$ with $ν$ integer).
background
The module derives the quantum Hall effect from the Recognition Science topological ledger. The integer quantum Hall effect (IQHE) is characterized by Hall conductance $σ_{xy} = n e^2/h$ where the integer $n$ is the Chern number of occupied Landau levels. The module doc states that this conductance is a topological invariant of the occupied levels and that the eight-tick balance constrains composite-fermion fractions in the fractional case.
proof idea
The proof is a term-mode construction. It applies the existential introduction by supplying the witness $n$ and discharges the equality subgoal with the reflexivity tactic.
why it matters
The result supports the module's key claim that $σ_{xy} = n e^2/h$ is quantized by an integer topological invariant. It aligns with the Recognition Science eight-tick octave (T7) that enforces integer Chern numbers via phase topology. The declaration touches the open question of recovering the exact von Klitzing constant from RS-native units (G = φ^5/π, ħ = φ^{-5}).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.