Prove2Me

The printed degrees of freedom and Birge ratios of the 2022 adjustment

Proved
CODATA.birge_printed

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

birgeratiochi-squarecodata2022degreesoffreedom

The two adjustments of the 2022 CODATA report have 133 - 79 = 54 and 16 - 1 = 15 degrees of freedom, and their final chi-squares are 44.2 and 12.9. The Birge ratio R_B = sqrt(chi^2/nu) is therefore sqrt(44.2/54) and sqrt(12.9/15), and the report prints 0.90 and 0.93. The milestone verifies these printed numbers by exact real arithmetic: the two subtractions hold exactly, and the two square roots lie in the rounding intervals [0.895, 0.905) and [0.925, 0.935) determined by the printed two-digit values.

Preamble
import Mathlib
import Definitions.Def_CODATA_lsa
import Definitions.Def_CODATA_uncert
import Definitions.Def_CODATA_values
Formal statement
/-!
# The printed degrees of freedom and Birge ratios

Section XII of the 2022 CODATA report records the arithmetic of the
two adjustments on which the recommended values are based: the main
adjustment of 133 input data for 79 adjusted constants, with
nu = N - M = 54 degrees of freedom and a final chi-square of 44.2, and
the separate adjustment of the sixteen values of the Newtonian
constant of gravitation, with 16 - 1 = 15 degrees of freedom and
chi-square 12.9; the Birge ratio R_B = sqrt(chi^2/nu) is printed as
0.90 for the main adjustment and 0.93 for the Newtonian constant. This
milestone verifies these printed numbers by exact real arithmetic: the
two subtractions, and the two rounding intervals that the printed
Birge ratios determine. This milestone is proved on the way to the
goal theorem `CODATA.codata_self_consistent`.
-/

namespace CODATA

/-- The degrees of freedom of the two adjustments of the 2022 CODATA
report are 133 - 79 = 54 and 16 - 1 = 15, and the Birge ratios
sqrt(44.2/54) and sqrt(12.9/15) round to the printed values 0.90 and
0.93: they lie in the intervals [0.895, 0.905) and [0.925, 0.935). -/
theorem birge_printed :
    dof 133 79 = 54 ∧ dof 16 1 = 15 ∧
      895/1000 ≤ Real.sqrt (442/10/54) ∧ Real.sqrt (442/10/54) < 905/1000 ∧
      925/1000 ≤ Real.sqrt (129/10/15) ∧ Real.sqrt (129/10/15) < 935/1000 := by
  sorry

end CODATA
Source
P. J. Mohr, D. B. Newell, B. N. Taylor and E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, J. Phys. Chem. Ref. Data 54, 033105 (2025), doi 10.1063/5.0279860; Rev. Mod. Phys. 97, 025002 (2025), doi 10.1103/RevModPhys.97.025002, section XII: nu = N - M = 54 for the main adjustment, 16 - 1 = 15 for the sixteen values of G, chi^2 = 44.2 and chi^2 = 12.9, R_B = sqrt(chi^2/nu) the Birge ratio, printed as 0.90 and 0.93.
Read-back

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

The formal statement is a closed conjunction of six arithmetic facts: dof 133 79 = 54 and dof 16 1 = 15, where dof N M is by definition N - M; and four inequalities over the reals: 0.895 is at most sqrt(44.2/54) which is less than 0.905, and 0.925 is at most sqrt(12.9/15) which is less than 0.935. The statement renders the intended milestone faithfully: the printed degrees of freedom of the two adjustments of the 2022 CODATA report, and the rounding intervals of the two Birge ratios that the printed values 0.90 and 0.93 determine. All quantities are exact decimals; no rounding is performed in the statement, only the interval inclusions.

Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph