E-line result is consistent with no variation at the $1.5\times10^{-7}$ level

Proved

MethanolMuDrift.eLine_two_sigma_level

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

fundamental-constantsmathematical-physicsstatistics

For the weighted least-squares fit of the three E lines (see the E-line fit milestone), with estimate $\widehat{\Delta\mu/\mu}=-b/c$ and statistical error $\sigma=\sigma_b/c$ , the estimate lies within two standard errors of zero and the two-standard-error bound equals $1.5\times10^{-7}$ to the stated precision:

\big|\widehat{\Delta\mu/\mu}\big|\le2\sigma,\qquad |2\sigma-1.5\times10^{-7}|\le0.05\times10^{-7}.

This is the paper's statement that the E-line result "is consistent with a non-varying $\mu$ at the level of $1.5\times10^{-7}$ (95% confidence level)".

Formalization Note The "95% confidence level" is rendered as the two-standard-error interval $\pm2\sigma$ (the usual Gaussian approximation); this reading is an interpretation, since the paper does not spell out the multiplier.

Preamble

import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift

Formal statement

namespace MethanolMuDrift

theorem eLine_two_sigma_level :
    |muDriftEstimate eK eV eSigma| ≤ 2 * muDriftStatErr eK eSigma ∧
      |2 * muDriftStatErr eK eSigma - 1.5e-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, p. 2 (left column): "... which is consistent with a non-varying μ at the level of 1.5×10^-7 (95% confidence level)."

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)$ , $V=(9.06,9.12,9.83)$ , $\sigma=(0.67,0.30,0.43)$ ), let $E=-b/299792.458$ (muDriftEstimate) and $s=\sqrt{S/\Delta}/299792.458$ (muDriftStatErr), with $b$ , $S$ , $\Delta$ the weighted least-squares quantities (weights $1/\sigma_i^2$ ). The statement asserts both

|E|\le 2s\qquad\text{and}\qquad |2s-1.5\times10^{-7}|\le 5\times10^{-9}.

It has no hypotheses and mentions no probability or confidence level; it is a 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

E-line result is consistent with no variation at the 1.5×10−71.5\times10^{-7}1.5×10−7 level

E-line result is consistent with no variation at the $1.5\times10^{-7}$ level