von_klitzing_constant
The von Klitzing constant is assigned the fixed value 25812.807 ohms as the resistance quantum R_K = h/e². Researchers deriving quantized Hall conductance from Chern numbers in the Recognition Science ledger cite this constant to fix the resistance scale. The assignment is a direct numerical definition with no lemmas or reductions applied.
claimThe von Klitzing constant equals 25812.807 ohms, where this value stands for the resistance quantum R_K = h/e².
background
The module sets the quantum Hall effect inside the Recognition Science topological ledger. Integer Hall conductance arises as the Chern number of occupied Landau levels, while fractional states follow from composite fermions under eight-tick balance. The von Klitzing constant supplies the resistance quantum that converts conductance quanta into observable resistance values.
proof idea
The declaration is a direct abbrev that performs a numerical assignment. No lemmas from the upstream edges are invoked; the constant is introduced as a primitive in the module.
why it matters in Recognition Science
This definition anchors the positivity result RK_positive and supplies the numerical base for quantized Hall conductance. It realizes the resistance quantum inside the RS framework, connecting directly to the Chern number integer theorem and the eight-tick phase topology described in the module paper RS_Quantum_Hall_Effect.tex.
scope and limits
- Does not derive the numerical value from RS primitives such as phi or J-cost.
- Does not address fractional quantum Hall states or Jain fractions.
- Does not connect the constant to Landau level energies or zero-point shifts.
Lean usage
theorem RK_positive : 0 < von_klitzing_constant := by norm_numformal statement (Lean)
68abbrev von_klitzing_constant : ℝ := 25812.807 -- Ohms
proof body
Definition body.
69
70/-- R_K is positive. -/