Prove2Me

The electronvolt is exact

Proved
SI.electronvolt_exact

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

electronvoltelementarychargeexactconversionmetrologysi

In every quantity model of the SI, the electronvolt - the kinetic energy acquired by an electron in passing through a potential difference of one volt - is exactly the volt multiplied by the defining-constant monomial of the elementary charge. In particular the conversion factor 1.602 176 634 × 10⁻¹⁹ between the electronvolt and the joule is exact (Table 8, note l): since Resolution 1 of the 26th CGPM fixed the numerical value of the elementary charge, no experimental uncertainty remains in this conversion.

Preamble
import Mathlib
import Definitions.Def_SI_dim
import Definitions.Def_SI_units
import Definitions.Def_SI_qmodel
Formal statement
/-!
# The electronvolt is exact

Table 8, note l of the SI Brochure: the electronvolt is the kinetic
energy acquired by an electron in passing through a potential
difference of one volt, 1 eV = 1.602 176 634 × 10⁻¹⁹ J, with the
conversion factor exact because the numerical value of the elementary
charge is fixed. In the quantity model, multiplying the volt by the
defining-constant monomial of the elementary charge yields exactly
the electronvolt. This milestone is proved on the way to the goal
theorem `SI.si_complete`.
-/

namespace SI

/-- In every quantity model of the SI, the electronvolt is the volt
scaled by the elementary charge:
toQ M eVolt = (the monomial e) · (toQ M volt). In particular, the
conversion factor 1.602 176 634 × 10⁻¹⁹ between the electronvolt and
the joule is exact (Table 8, note l). -/
theorem electronvolt_exact (M : SIModel) :
    toQ M eVolt = qmul (⟨1, eC Const.e⟩ : QMono) (toQ M volt) := by
  sorry

end SI
Source
The International System of Units (SI), 9th edition, V4.01 (BIPM, 2026), chapter 4, Table 8, note l (the electronvolt; the exactness of its conversion factor following the fixing of the elementary charge), with section 2.2, Table 1.
Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

The formal statement says that under any model M of the seven defining statements, the identifying image of the electronvolt - defined as the joule scaled by the exact rational 1602176634/10²⁸, which is the fixed numerical value of the elementary charge - equals the product of the monomial e (with coefficient one) and the identifying image of the volt. Read physically: one electronvolt is the energy of one elementary charge moved through one volt, so the eV-to-J factor 1.602 176 634 × 10⁻¹⁹ is exact. This is precisely note l of Table 8; no approximation or experimental quantity enters the statement.

View graph