The line fit of $V$ against $K_\mu$ recovers $\Delta\mu/\mu$ from noise-free data

Proved

MethanolMuDrift.wls_recovers_exact_drift

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

fundamental-constantsmathematical-physicsstatistics

Let $n$ points carry sensitivity coefficients $K_1,\dots,K_n$ and nonzero uncertainties $\sigma_1,\dots,\sigma_n$ , and assume the $K_i$ are not all equal. Suppose the line positions obey the paper's velocity relation $V/c=-K_\mu\,\Delta\mu/\mu$ exactly, up to a common velocity offset $a$ :

V_i = a - c\,\delta\,K_i\qquad(i=1,\dots,n),

where $\delta$ plays the role of $\Delta\mu/\mu$ . Then the weighted least-squares straight-line fit of $V$ against $K_\mu$ (weights $1/\sigma_i^2$ ) returns exactly these parameters: the derived estimate $-b/c$ equals $\delta$ and the fitted intercept equals $a$ ,

-\frac{b}{c}=\delta,\qquad a_{\mathrm{fit}}=a .

This is the consistency property behind Fig. 3: fitting a line to the observed positions plotted against $K_\mu$ and reading off its slope measures $\Delta\mu/\mu$ .

Formalization Note The uncertainties only need to be nonzero (weights $1/\sigma_i^2>0$ ); the non-constancy of $K$ guarantees that the normal equations are nondegenerate. Velocities and $c$ are in km/s.

Preamble

import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift

Formal statement

namespace MethanolMuDrift

theorem wls_recovers_exact_drift {n : ℕ} (K σ : Fin n → ℝ) (hσ : ∀ i, σ i ≠ 0)
    (hK : ∃ i j, K i ≠ K j) (a δ : ℝ) :
    muDriftEstimate K (fun i => a - speedOfLight * δ * K i) σ = δ ∧
      wlsIntercept K (fun i => a - speedOfLight * δ * K i) σ = a := 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 velocities between different transitions are interrelated via V/c = -KμΔμ/μ ... to determine the fractional change in μ, the peak positions of the four transitions are plotted (in V/c) versus Kμ, and a (dashed) line is fitted to the data (Fig. 3)."

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).

For every natural number $n$ , all families $K=(K_i)$ and $\sigma=(\sigma_i)$ of reals indexed by $i\in\{0,\dots,n-1\}$ , and all reals $a,\delta$ , assume

$\sigma_i\neq 0$ for every $i$ ;
there exist indices $i,j$ with $K_i\neq K_j$ (so in particular $n\ge 2$ ).

Define $V_i = a - 299792.458\cdot\delta\cdot K_i$ . Then both of the following hold:

$-\,b/299792.458=\delta$ , where $b$ is the weighted least-squares slope wlsSlope $(K,V,\sigma)=(S S_{KV}-S_KS_V)/(S S_{KK}-S_K^2)$ with weights $1/\sigma_i^2$ (definition file);
the weighted least-squares intercept wlsIntercept $(K,V,\sigma)=(S_{KK}S_V-S_KS_{KV})/(S S_{KK}-S_K^2)$ equals $a$ .

No positivity of $\sigma_i$ is assumed, only $\sigma_i\neq0$ ; the weights depend on $\sigma_i^2$ .

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

The line fit of VVV against KμK_\muKμ​ recovers Δμ/μ\Delta\mu/\muΔμ/μ from noise-free data

The line fit of $V$ against $K_\mu$ recovers $\Delta\mu/\mu$ from noise-free data