Prove2Me

Fit of all four lines: Δμ/μ=(11.0±6.8)×10−8\Delta\mu/\mu=(11.0\pm6.8)\times10^{-8}, χν2≈6.4\chi^2_\nu\approx6.4

Proved
MethanolMuDrift.allLine_fit

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

fundamental-constantsmathematical-physicsstatistics

Fit a straight line, by weighted least squares with weights 1/σi21/\sigma_i^2, to all four methanol lines of Table 1 plotted against their sensitivity coefficients:

(Kμ, V±σ)∈{(−32.8, 9.06±0.67), (−1, 8.40±0.10), (−1, 9.12±0.30), (−7.4, 9.83±0.43)}(km/s).(K_\mu,\,V\pm\sigma)\in\{(-32.8,\,9.06\pm0.67),\,(-1,\,8.40\pm0.10),\,(-1,\,9.12\pm0.30),\,(-7.4,\,9.83\pm0.43)\}\quad(\text{km/s}).

With slope bb, slope standard error σb\sigma_b and reduced chi-squared χν2\chi^2_\nu (two degrees of freedom),

∣−bc−11.0×10−8∣≤0.5×10−8,∣σbc−6.8×10−8∣≤0.1×10−8,∣χν2−6.4∣≤0.2.\Big|{-\tfrac{b}{c}}-11.0\times10^{-8}\Big|\le0.5\times10^{-8},\qquad\Big|\tfrac{\sigma_b}{c}-6.8\times10^{-8}\Big|\le0.1\times10^{-8},\qquad|\chi^2_\nu-6.4|\le0.2 .

This corresponds to the paper's four-line result Δμ/μ=(11.0±6.8)×10−8\Delta\mu/\mu=(11.0\pm6.8)\times10^{-8} with "a much larger χν2\chi^2_\nu of 6.4", which motivated discarding the A line from the fiducial fit.

Formalization Note Recomputation from the rounded Table 1 entries gives ≈11.35×10−8\approx11.35\times10^{-8}, ≈6.84×10−8\approx6.84\times10^{-8} and χν2≈6.27\chi^2_\nu\approx6.27, slightly different from the printed values (presumably computed from unrounded positions). The tolerances 0.5×10−80.5\times10^{-8}, 0.1×10−80.1\times10^{-8} and 0.20.2 were chosen to cover this rounding gap; they are a formalization choice, not stated in the paper.

Preamble
import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift
Formal statement
namespace MethanolMuDrift

theorem allLine_fit :
    |muDriftEstimate allK allV allSigma - 11.0e-8| ≤ 0.5e-8 ∧
      |muDriftStatErr allK allSigma - 6.8e-8| ≤ 0.1e-8 ∧
      |wlsReducedChiSq allK allV allSigma - 6.4| ≤ 0.2 := by sorry

end MethanolMuDrift
Source
J. Bagdonaite, P. Jansen, C. Henkel, H. L. Bethlem, K. M. Menten, W. Ubachs, "A Stringent Limit on a Drifting Proton-to-Electron Mass Ratio from Alcohol in the Early Universe", Science (First Release, 13 December 2012), doi:10.1126/science.1224898, https://doi.org/10.1126/science.1224898, p. 2 (left column): "The fit on all four transitions has a much larger χν² of 6.4 ... and it delivers Δμ/μ = (11.0 ± 6.8) × 10^-8."; data from Table 1, p. 4.
Read-back

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

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, at the explicit request of the account owner. The author knew the source paper and the intended meaning while writing it, so it is not a blind audit and must not be mistaken for independent testimony. Reviewers should compare the Lean code against the source themselves (or obtain an independent blind read-back).

With the four-point data of the definition file — K=(−32.8,−1,−1,−7.4)K=(-32.8,-1,-1,-7.4), V=(9.06,8.40,9.12,9.83)V=(9.06,8.40,9.12,9.83), σ=(0.67,0.10,0.30,0.43)\sigma=(0.67,0.10,0.30,0.43) — let bb, σb=S/Δ\sigma_b=\sqrt{S/\Delta} and χν2=χ2/(4−2)\chi^2_\nu=\chi^2/(4-2) be the weighted least-squares slope, slope standard error and reduced chi-squared (weights 1/σi21/\sigma_i^2), and c=299792.458c=299792.458. The statement asserts all three inequalities

∣−bc−1.1×10−7∣≤5×10−9,∣σbc−6.8×10−8∣≤1×10−9,∣χν2−6.4∣≤0.2.\left|-\frac{b}{c}-1.1\times10^{-7}\right|\le5\times10^{-9},\qquad\left|\frac{\sigma_b}{c}-6.8\times10^{-8}\right|\le1\times10^{-9},\qquad|\chi^2_\nu-6.4|\le0.2 .

It has no hypotheses.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

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

View graph