IndisputableMonolith.Physics.QuantumHallEffect
Module packaging integer and fractional quantum Hall structure in Recognition Science units. It defines Chern numbers as integer topological invariants, ties Hall conductance quantization to the eight-tick clock, and records the von Klitzing constant, Landau level energies, and Jain composite-fermion fractions. Condensed-matter or RS-constants workers would cite it for the IQHE/FQHE dictionary. Content is mostly definitions plus integrality and positivity lemmas built on EightTick and J-cost.
claimToolkit for the quantum Hall effect: Chern number $C\in\mathbb{Z}$ equal to the number of filled Landau levels (IQHE) or the composite-fermion Landau structure (FQHE); Hall conductance $\sigma_{xy}=C\,e^{2}/h$; von Klitzing constant $R_K>0$; Landau energies, level spacing, and zero-point energy; Jain filling fractions with odd denominators.
background
Recognition Science runs on a discrete eight-tick clock (period $2^3$), with phases $0,\pi/4,\ldots,7\pi/4$. That octave is the natural place to force integrality of topological indices that count filled bands. The module imports the EightTick foundation and the J-cost compatibility surface (re-export of the canonical cost $J$), so Hall quantities sit in the same discrete-time and cost language as the rest of the monolith.
In the integer quantum Hall effect, the transverse conductance is quantized in units of $e^{2}/h$, with the integer equal to a Chern number of the filled Landau levels. In the fractional case, Jain's composite-fermion construction maps fractions to an effective integer problem; the module records the corresponding filling and denominator constraints.
The supplied module doc frames a Chern number as an integer-valued topological invariant that, in QHE, equals filled Landau levels (IQHE) or the composite-fermion Landau structure (FQHE). Sibling names cover conductance quantization, eight-tick integrality of Chern numbers, IQHE filling and integer conductance, $R_K$ positivity, Landau energetics, and Jain fractions.
proof idea
Definition-heavy physics module, not a single theorem. It introduces ChernNumber and related Hall quantities, then supplies short lemmas: integrality of the Chern number from the eight-tick structure, IQHE filling and integer conductance, positivity of the von Klitzing constant, Landau energy/spacing/zero-point formulas, and Jain fraction denominator constraints. Argument shape is dictionary plus elementary algebraic or positivity checks on top of EightTick and J-cost imports, rather than a long derivation chain.
why it matters in Recognition Science
Places IQHE/FQHE inside the RS discrete-time and cost framework so Hall quantization can be cited next to the eight-tick octave (forcing-chain T7) rather than as an external condensed-matter fact. Downstream usage is not yet wired in the graph (no used_by edges), so the module is a physics surface for later transport, metrology, or constants work. The Chern-from-8tick lemma is the conceptual bridge: topological integers arise from the same period-$8$ clock that forces the octave elsewhere in the monolith. Von Klitzing and Jain pieces give the standard experimental anchors (quantized $R_K$, odd-denominator fractions) in RS-native packaging.
scope and limits
- Does not derive microscopic many-body wavefunctions or Laughlin/Jain trial states.
- Does not prove experimental metrology bounds on $R_K$ beyond positivity and definitions.
- Does not treat disordered or interacting edge modes beyond Chern/filling bookkeeping.
- Does not connect Hall data to the alpha band or mass ladder formulas.
- Does not supply used_by consumers yet; module is a standalone physics surface.
depends on (2)
declarations in this module (22)
-
structure
ChernNumber -
theorem
hall_conductance_quantized -
theorem
chern_number_integer_from_8tick -
def
iqhe_filling -
theorem
iqhe_conductance_integer -
abbrev
von_klitzing_constant -
theorem
RK_positive -
def
landau_energy -
theorem
landau_spacing -
theorem
zero_point_energy -
def
jain_fraction -
theorem
jain_denominator_odd_plus -
theorem
jain_denominator_odd_minus -
theorem
fqhe_odd_denominator -
theorem
one_third_in_jain_sequence -
theorem
two_fifth_in_jain_sequence -
def
laughlin_quasi_charge -
theorem
laughlin_charge_one_third -
theorem
quasi_charge_decreasing -
def
laughlin_exchange_phase -
theorem
electron_exchange_phase -
theorem
one_third_exchange_phase