Prove2Me

Fit of the three E lines: Δμ/μ=(−0.1±7.6)×10−8\Delta\mu/\mu=(-0.1\pm7.6)\times10^{-8}, χν2≈2.0\chi^2_\nu\approx2.0

Proved
MethanolMuDrift.eLine_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 the positions of the three E-symmetry methanol lines of Table 1 plotted against their sensitivity coefficients:

(Kμ, V±σ)∈{(−32.8,  9.06±0.67),  (−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,\;9.12\pm0.30),\;(-7.4,\;9.83\pm0.43)\}\quad(\text{km/s}).

Let bb be the fitted slope, σb\sigma_b its standard error and χν2\chi^2_\nu the reduced chi-squared (one degree of freedom). Then the derived estimate Δμ/μ=−b/c\Delta\mu/\mu=-b/c, its statistical error σb/c\sigma_b/c and χν2\chi^2_\nu reproduce the paper's values to the stated precision:

∣−bc−(−0.1×10−8)∣≤0.05×10−8,∣σbc−7.6×10−8∣≤0.1×10−8,∣χν2−2.0∣≤0.05.\Big|{-\tfrac{b}{c}}-(-0.1\times10^{-8})\Big|\le0.05\times10^{-8},\qquad \Big|\tfrac{\sigma_b}{c}-7.6\times10^{-8}\Big|\le0.1\times10^{-8},\qquad |\chi^2_\nu-2.0|\le0.05 .

This is the paper's fiducial measurement Δμ/μ=(−0.1±7.6)×10−8\Delta\mu/\mu=(-0.1\pm7.6)\times10^{-8} with χν2∼2.0\chi^2_\nu\sim2.0.

Formalization Note The paper reports rounded values computed from unrounded data; recomputation from the rounded Table 1 entries gives σb/c≈7.69×10−8\sigma_b/c\approx7.69\times10^{-8}, so the tolerance on the error is 0.1×10−80.1\times10^{-8} rather than a half unit of the last digit. Tolerances on the estimate and on χν2\chi^2_\nu are a half unit of the last reported digit.

Preamble
import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift
Formal statement
namespace MethanolMuDrift

theorem eLine_fit :
    |muDriftEstimate eK eV eSigma - (-0.1e-8)| ≤ 0.05e-8 ∧
      |muDriftStatErr eK eSigma - 7.6e-8| ≤ 0.1e-8 ∧
      |wlsReducedChiSq eK eV eSigma - 2.0| ≤ 0.05 := 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 analysis of the E transitions results in Δμ/μ = (-0.1 ± 7.6)×10^-8 ... The reduced chi-squared, χν², ... is ~2.0"; 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 data of the definition file — K=(−32.8,−1,−7.4)K=(-32.8,-1,-7.4), V=(9.06,9.12,9.83)V=(9.06,9.12,9.83), σ=(0.67,0.30,0.43)\sigma=(0.67,0.30,0.43) (three points) — let bb, σb=S/Δ\sigma_b=\sqrt{S/\Delta} and χν2=χ2/(3−2)=χ2\chi^2_\nu=\chi^2/(3-2)=\chi^2 be the weighted least-squares slope, slope standard error and reduced chi-squared with weights 1/σi21/\sigma_i^2, and c=299792.458c=299792.458. The statement asserts all three inequalities

∣−bc+1×10−9∣≤5×10−10,∣σbc−7.6×10−8∣≤1×10−9,∣χν2−2∣≤0.05.\left|-\frac{b}{c}+1\times10^{-9}\right|\le 5\times10^{-10},\qquad \left|\frac{\sigma_b}{c}-7.6\times10^{-8}\right|\le 1\times10^{-9},\qquad \left|\chi^2_\nu-2\right|\le0.05 .

It has no hypotheses; it is a closed statement about specific numbers.

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