Pure rotational transitions have $K_\mu=-1$

Proved

MethanolMuDrift.rotational_sensitivity_eq_neg_one

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

fundamental-constantsmathematical-physicsstatistics

Let $C\neq 0$ be a constant and let a transition frequency depend on the proton-to-electron mass ratio $\mu$ as

\nu(\mu)=\frac{C}{\mu},

i.e. it is inversely proportional to $\mu$ , as is the case for pure rotational transitions (whose frequency is inversely proportional to the reduced mass of the molecule). Then at every $\mu>0$ its sensitivity coefficient $K_\mu=\frac{\mu}{\nu}\frac{d\nu}{d\mu}$ equals

K_\mu=-1 .

This is the value used for the two $0_0$ – $1_0$ lines ( $A^+$ and $E$ ) in Table 1 and serves as the reference point against which the enhanced sensitivities of mixed torsion–rotation transitions are compared.

Formalization Note The sensitivity coefficient is the logarithmic derivative $(\mu/\nu(\mu))\,\nu'(\mu)$ from the definition file; the model "frequency proportional to $1/\mu$ " is taken as the hypothesis, exactly as stated in the paper.

Preamble

import Mathlib
import Definitions.Def_Bagdonaite2013_MethanolMuDrift

Formal statement

namespace MethanolMuDrift

theorem rotational_sensitivity_eq_neg_one (C μ : ℝ) (hC : C ≠ 0) (hμ : 0 < μ) :
    sensitivityCoeff (fun m => C / m) μ = -1 := 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. 1 (right column): definition

\Delta\nu/\nu=K_\mu\,\Delta\mu/\mu

and "the frequency of pure rotational transitions ... are inversely proportional to the reduced mass of methanol and hence to the proton-to-electron mass ratio. Consequently, these have sensitivity coefficients equal to -1."

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 all real numbers $C$ and $\mu$ such that

$C\neq 0$ , and
$\mu>0$ ,

consider the function $\nu(m)=C/m$ (with Lean's convention $C/0=0$ , irrelevant here since only a neighbourhood of $\mu>0$ matters for the derivative). The statement asserts

\frac{\mu}{\nu(\mu)}\cdot \nu'(\mu) = -1,

where $\nu'(\mu)$ is the derivative of $m\mapsto C/m$ at $\mu$ (Lean's deriv) and the left side is exactly the definition-file quantity sensitivityCoeff. No other hypotheses are present.

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

Pure rotational transitions have Kμ=−1K_\mu=-1Kμ​=−1

Pure rotational transitions have $K_\mu=-1$