RK_positive
plain-language theorem explainer
The declaration establishes that the von Klitzing constant is strictly positive. Researchers modeling the integer quantum Hall effect within Recognition Science would cite this basic positivity result when normalizing conductances or resistances. The proof is a direct numerical normalization that confirms the constant exceeds zero without further computation.
Claim. $R_K > 0$, where $R_K$ is the von Klitzing constant arising as the resistance quantum in the topological ledger for the quantum Hall effect.
background
The Quantum Hall Effect module derives the integer quantum Hall conductance from Chern numbers of occupied Landau levels under the eight-tick phase constraint, with the fractional case following from composite fermions and odd-denominator restrictions. The von Klitzing constant enters as the fundamental resistance scale. Upstream results supply the tick as the fundamental time quantum (equal to 1 in RS-native units) and the eight-tick phase as multiples of π/4, both used to anchor the topological invariants.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to the inequality 0 < von_klitzing_constant, reducing it to a direct numerical comparison that holds by the constant's definition.
why it matters
This positivity result underpins the quantization theorems in the same module, including hall_conductance_quantized and chern_number_integer, by guaranteeing that resistances remain positive when conductances are expressed in units of e²/h. It aligns with the eight-tick octave and the positive constants fixed in RS-native units (c = 1, ħ = φ^{-5}). No open scaffolding is closed here; the result is a terminal numerical check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.