Prove2Me

The 000_0–101_0A+A^+ and EE lines are separated by 0.72±0.320.72\pm0.32 km/s

Proved
MethanolMuDrift.A_E_separation

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

fundamental-constantsmathematical-physicsstatistics

In Table 1 the 000_0–10 E1_0\,E line is at 9.12±0.309.12\pm0.30 km/s and the 000_0–10 A+1_0\,A^+ line at 8.40±0.108.40\pm0.10 km/s. Their separation and its uncertainty (independent errors added in quadrature) are

9.12−8.40=0.72,∣0.302+0.102−0.32∣≤0.005,9.12-8.40=0.72,\qquad \Big|\sqrt{0.30^2+0.10^2}-0.32\Big|\le0.005,

i.e. the two lines are separated by 0.72±0.320.72\pm0.32 km/s. Together with the larger E linewidths, this is the evidence for spatial segregation of E- and A-symmetry methanol that led the authors to adopt the E-only fit as fiducial.

Formalization Note Positions and uncertainties are read from the definition file's Table 1 arrays (indices 2 and 1); the quadrature rule for the uncertainty of a difference is the reading of "±0.32\pm0.32" used here.

Preamble
import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift
Formal statement
namespace MethanolMuDrift

theorem A_E_separation :
    allV 2 - allV 1 = 0.72 ∧
      |Real.sqrt (allSigma 2 ^ 2 + allSigma 1 ^ 2) - 0.32| ≤ 0.005 := 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 (right column): "In the combined spectrum the 0_0-1_0 A+ and 0_0-1_0 E transitions ... are separated by 0.72 ± 0.32 km/s."; 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).

Using the definition-file arrays allV =(9.06,8.40,9.12,9.83)=(9.06,8.40,9.12,9.83) and allSigma =(0.67,0.10,0.30,0.43)=(0.67,0.10,0.30,0.43) (indices 0..30..3), the statement asserts

  1. V2−V1=0.72V_2-V_1=0.72, i.e. 9.12−8.40=0.729.12-8.40=0.72;
  2. ∣σ22+σ12−0.32∣≤0.005\left|\sqrt{\sigma_2^2+\sigma_1^2}-0.32\right|\le0.005, i.e. ∣0.302+0.102−0.32∣≤0.005\left|\sqrt{0.30^2+0.10^2}-0.32\right|\le0.005.

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