Shift of the – line between epochs: km/s
ProvedMethanolMuDrift.variability_shiftThe strong – line was measured at km/s in December 2011 and at km/s in April 2012. The difference and its uncertainty (errors added in quadrature) are
i.e. km/s — the "possibly indicative" systematic shift due to time variability of the background source, which the authors convert into the conservative systematic uncertainty on .
Formalization Note The two epoch positions are not part of Table 1 and are written directly into the statement.
import Mathlib import Definitions.Def_Bagdonaite2013_MethanolMuDrift
namespace MethanolMuDrift
theorem variability_shift :
(8.80 : ℝ) - 8.32 = 0.48 ∧ Real.sqrt ((0.24 : ℝ) ^ 2 + 0.10 ^ 2) = 0.26 := by sorry
end MethanolMuDrift
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).
A closed statement about real numbers with no hypotheses:
- ;
- (the real square root).
It does not reference any definition from the definition file.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.