Registry · Definition IV.D27 established formalized

IV.D27 — SI Measured Constants

9 CODATA 2022 measured constants: m_n, m_e, m_p, 1/α, sin²θ_W, α_s(M_Z), R=m_n/m_e, Δm(n-p), G. All stored as (numer, denom) Nat pairs with positive denominators.

Book IV Part 2 Ch. 12

Dependency Graph

Depends on (1)

Depended on by (5)

Lean Formalization

Module: TauLib.BookIV.Calibration.SIReference

Symbol: Tau.BookIV.Calibration.si_measured_constants