Prove2Me

Main result: Δμ/μ=(0.0±1.0)×10−7\Delta\mu/\mu=(0.0\pm1.0)\times10^{-7} at z=0.89z=0.89

Proved
MethanolMuDrift.combined_limit

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

fundamental-constantsmathematical-physicsstatistics

Let Δμ/μ^=−b/c\widehat{\Delta\mu/\mu}=-b/c and σstat=σb/c\sigma_{\mathrm{stat}}=\sigma_b/c be the estimate and statistical error obtained from the weighted least-squares fit of the three E-symmetry methanol lines of Table 1 (positions plotted against sensitivity coefficients KμK_\mu), and let σsys=7.0×10−8\sigma_{\mathrm{sys}}=7.0\times10^{-8} be the systematic uncertainty adopted for source variability. Adding the two uncertainties in quadrature, the result rounds to the paper's headline limit Δμ/μ=(0.0±1.0)×10−7\Delta\mu/\mu=(0.0\pm1.0)\times10^{-7}:

∣Δμ/μ^∣<0.05×10−7,∣σstat2+σsys2−1.0×10−7∣<0.05×10−7.\big|\widehat{\Delta\mu/\mu}\big|<0.05\times10^{-7},\qquad\Big|\sqrt{\sigma_{\mathrm{stat}}^2+\sigma_{\mathrm{sys}}^2}-1.0\times10^{-7}\Big|<0.05\times10^{-7}.

This is the constraint on a cosmological variation of the proton-to-electron mass ratio at redshift z=0.89z=0.89 (look-back time about 7 billion years), consistent with a null result.

Formalization Note The systematic uncertainty 7.0×10−87.0\times10^{-8} is an input taken from the paper (it comes from a model of source variability that is not reproduced here). The strict inequalities express "rounds to one decimal in units of 10−710^{-7}".

Preamble
import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift
Formal statement
namespace MethanolMuDrift

theorem combined_limit :
    |muDriftEstimate eK eV eSigma| < 0.05e-7 ∧
      |Real.sqrt (muDriftStatErr eK eSigma ^ 2 + muDriftSysErr ^ 2) - 1.0e-7| < 0.05e-7 := 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, Abstract (p. 1) and p. 2 (right column): "we obtain a limit on varying μ to be Δμ/μ = (-0.1 ± 7.6stat ± 7.0sys) ×10^-8 or, if the statistical and systematic uncertainties are added in quadrature, a limit of Δμ/μ = (0.0 ± 1.0)×10^-7."; 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 E-line 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)), let

  • E=−b/299792.458E=-b/299792.458 where b=(SSKV−SKSV)/(SSKK−SK2)b=(SS_{KV}-S_KS_V)/(SS_{KK}-S_K^2) is the weighted least-squares slope (weights 1/σi21/\sigma_i^2);
  • s=S/(SSKK−SK2)/299792.458s=\sqrt{S/(SS_{KK}-S_K^2)}/299792.458;
  • ssys=7.0×10−8s_{\mathrm{sys}}=7.0\times10^{-8} (muDriftSysErr).

The statement asserts both strict inequalities

∣E∣<5×10−9and∣s2+ssys2−1.0×10−7∣<5×10−9.|E|<5\times10^{-9}\qquad\text{and}\qquad\left|\sqrt{s^2+s_{\mathrm{sys}}^2}-1.0\times10^{-7}\right|<5\times10^{-9}.

No hypotheses; a closed statement about specific real 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