A single relative-uncertainty witness for the alpha family
ProvedCODATA.alpha_familyIn the 2022 CODATA adjustment the fine-structure constant alpha, its inverse, the vacuum magnetic permeability mu_0, the vacuum electric permittivity eps_0 and the impedance of vacuum Z_0 form a family determined by alpha, all other factors being exact. Their printed uncertainties in Table XXXIII carry two significant digits: alpha = 7.297 352 5643(11) x 10^-3, 1/alpha = 137.035 999 177(21), mu_0 = 1.256 637 061 27(20) x 10^-6, eps_0 = 8.854 187 8188(14) x 10^-12, Z_0 = 376.730 313 412(58). The milestone verifies the joint consistency of these five printed uncertainty statements: there is a single rational relative uncertainty ur, of order 1.6 x 10^-10, such that ur times each of the five rational values lies in the rounding interval determined by the printed two-digit uncertainty.
import Mathlib import Definitions.Def_CODATA_lsa import Definitions.Def_CODATA_uncert import Definitions.Def_CODATA_values
/-!
# A single relative-uncertainty witness for the alpha family
In the 2022 CODATA adjustment the vacuum magnetic permeability, the
vacuum electric permittivity, the impedance of vacuum and the two
fine-structure-constant entries form a family: mu_0 = 2 alpha h/(e² c),
eps_0, Z_0 and alpha are mutually determined, the other factors being
exact. Their printed uncertainties in Table XXXIII (two significant
digits) are therefore all products of a single relative uncertainty
with the respective exact values: alpha = 7.297 352 5643(11) × 10⁻³,
1/alpha = 137.035 999 177(21), mu_0 = 1.256 637 061 27(20) × 10⁻⁶,
eps_0 = 8.854 187 8188(14) × 10⁻¹², Z_0 = 376.730 313 412(58). This
milestone verifies the consistency of these five printed uncertainty
statements by exact rational arithmetic: there is a single rational
relative-uncertainty witness ur, of order 1.6 × 10⁻¹⁰, such that ur
times each of the five rational values lies in the rounding interval
determined by the printed two-digit uncertainty. This milestone is
proved on the way to the goal theorem
`CODATA.codata_self_consistent`.
-/
namespace CODATA
/-- There is a single rational relative uncertainty ur with
1.55 × 10⁻¹⁰ ≤ ur < 1.65 × 10⁻¹⁰ such that ur alpha lies in
[1.05, 1.15) × 10⁻¹², ur/alpha lies in [2.05, 2.15) × 10⁻⁸,
ur mu_0 lies in [1.95, 2.05) × 10⁻¹⁶, ur eps_0 lies in
[1.35, 1.45) × 10⁻²¹ and ur Z_0 lies in [5.85, 5.95) × 10⁻⁸: one
witness reproduces the printed two-significant-digit uncertainties of
the whole alpha family of the 2022 adjustment. -/
theorem alpha_family :
∃ ur : ℚ,
155/(10:ℚ)^12 ≤ ur ∧ ur < 165/(10:ℚ)^12 ∧
105/(10:ℚ)^14 ≤ ur * alphaVal ∧ ur * alphaVal < 115/(10:ℚ)^14 ∧
205/(10:ℚ)^10 ≤ ur * alphaInvVal ∧
ur * alphaInvVal < 215/(10:ℚ)^10 ∧
195/(10:ℚ)^18 ≤ ur * mu0Val ∧ ur * mu0Val < 205/(10:ℚ)^18 ∧
135/(10:ℚ)^23 ≤ ur * eps0Val ∧ ur * eps0Val < 145/(10:ℚ)^23 ∧
585/(10:ℚ)^10 ≤ ur * z0Val ∧ ur * z0Val < 595/(10:ℚ)^10 := by
sorry
end CODATA
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The formal statement is existential: there exists a rational number ur with 155/10^12 at most ur, ur less than 165/10^12 (that is, ur is of order 1.55 to 1.65 times 10^-10), such that five rational interval inclusions hold simultaneously: ur times alpha lies in [105/10^14, 115/10^14); ur times the inverse of alpha lies in [205/10^10, 215/10^10); ur times mu_0 lies in [195/10^18, 205/10^18); ur times eps_0 lies in [135/10^23, 145/10^23); and ur times Z_0 lies in [585/10^10, 595/10^10). Here alpha, 1/alpha, mu_0, eps_0 and Z_0 are the rational recommended values of the 2022 adjustment recorded in the definitions. The statement renders the intended milestone faithfully: one relative-uncertainty witness jointly reproduces the five printed two-significant-digit uncertainties of the alpha family; the witness is supplied by the prover, for example ur = 156/10^12.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.