Prove2Me

KJ2RK=4/hK_J^2R_K = 4/h

Proved
CODATA2022.josephson_sq_mul_vonKlitzing

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysismathematical-physicsmetrology

The Josephson and von Klitzing constants of Table XXXII, KJ=2e/hK_J = 2e/h and RK=h/e2R_K = h/e^2, satisfy the identity used in electrical metrology to realize the watt:

KJ2RK  =  4e2h2⋅he2  =  4h.K_J^2R_K \;=\; \frac{4e^2}{h^2}\cdot\frac{h}{e^2} \;=\; \frac{4}{h}.

Since ee and hh are fixed exactly, both constants and their combination are exact.

Preamble
import Mathlib
import Definitions.Def_CODATA2022_si_defining_constants
import Definitions.Def_CODATA2022_radiation_constants
open MeasureTheory
Formal statement
namespace CODATA2022
theorem josephson_sq_mul_vonKlitzing :
    josephsonConstant ^ 2 * vonKlitzingConstant = 4 / planckConstant := by sorry
end CODATA2022
Source
Mohr, Newell, Taylor, Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, Rev. Mod. Phys. 97, 025002 (2025), https://doi.org/10.1103/RevModPhys.97.025002, Table XXXII: Josephson constant KJ=2e/hK_J = 2e/h and von Klitzing constant RK=μ0c/2α=2πℏ/e2R_K = \mu_0c/2\alpha = 2\pi\hbar/e^2.
Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (same agent as the drafter; non-blind)

Disclosure - non-blind read-back. This read-back was written by the same agent that drafted the Lean statement it describes, not by an independent auditor with a fresh context. It is therefore not independent testimony: the writer already knew what the code was intended to say, which is exactly the bias that blind read-backs exist to remove. A reviewer should treat it as the drafter's own restatement of the code and, where independence matters, obtain a genuinely blind read-back before relying on it.

With e=1.602176634×10−19e = 1.602176634\times10^{-19} and h=6.62607015×10−34h = 6.62607015\times10^{-34} the fixed numbers of the definition file, and KJ=2e/hK_J = 2e/h, RK=h/e2R_K = h/e^2, the statement asserts the equality of two real numbers, with no variables and no hypotheses:

(2eh)2⋅he2  =  4h.\left(\frac{2e}{h}\right)^2\cdot\frac{h}{e^2} \;=\; \frac{4}{h}.

All denominators are nonzero rationals, so no degenerate division arises. The identity is algebraic: it holds for every nonzero ee and hh, and does not use the particular values fixed by the SI.

View graph