Physics Quantum Hall Effect

Quantum Hall Effect

The quantum Hall effect is a physical phenomenon observed in a two-dimensional electron gas subjected to a strong perpendicular magnetic field at low temperature. The Hall conductance σ_xy is measured to be an integer multiple of e²/h, the conductance quantum, a fact that is independent of the sample's details. In Recognition Science, this quantization is not an accident of material physics but a direct consequence of the eight-tick cycle, the fundamental recognition cycle that forces the integer structure of topological invariants.

The module establishes that the Chern number, the topological invariant that classifies the quantized Hall plateaus, is integer-valued by definition. The theorem `chern_number_integer_from_8tick` proves that the eight-tick phase, where the eighth power of the phase equals one, forces integer winding numbers. This provides the topological foundation for the integer quantum Hall effect. The Hall conductance itself is then proven to be an integer multiple of the conductance quantum, as stated in `hall_conductance_quantized`.

For the fractional quantum Hall effect, the module derives the allowed filling fractions. The Jain sequence, ν = p/(2mp ± 1), is defined, and the theorem `fqhe_odd_denominator` proves that the denominators in this sequence are always odd. This odd denominator requirement is a direct consequence of the antisymmetry of fermion exchange, captured in the theorem `electron_exchange_phase` which shows the exchange phase for an electron is π. The Laughlin quasi-particle charge at filling ν = 1/q is defined as 1/q, and the theorem `laughlin_charge_one_third` proves this equals 1/3 for q = 3, matching the most famous fractional state.

The Landau level structure is also established. The energy of a Landau level is defined as ω_c(n + 1/2), and the theorem `landau_spacing` proves the spacing between adjacent levels is exactly the cyclotron frequency ω_c. The zero-point energy, the energy of the lowest Landau level, is proven to be ω_c/2 by the theorem `zero_point_energy`. These results provide the energy scale for the quantum Hall effect within the Recognition Science framework.

THEOREM ChernNumber · chern_number_integer_from_8tick · IndisputableMonolith/Physics/QuantumHallEffect.lean

THEOREM hall_conductance_quantized · IndisputableMonolith/Physics/QuantumHallEffect.lean

THEOREM fqhe_odd_denominator · IndisputableMonolith/Physics/QuantumHallEffect.lean

THEOREM laughlin_charge_one_third · IndisputableMonolith/Physics/QuantumHallEffect.lean

THEOREM landau_spacing · IndisputableMonolith/Physics/QuantumHallEffect.lean

THEOREM zero_point_energy · IndisputableMonolith/Physics/QuantumHallEffect.lean

What this page does not claim

This module does not derive the numerical value of the von Klitzing constant from first principles; it only defines it as 25812.807 ohms. This module does not prove that the fractional quantum Hall effect is observed in any specific material. This module does not claim that the physical recognition-to-linking bridge for the quantum Hall effect is fully established.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/QuantumHallEffect.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: