LMC: 1.2% distance uncertainty, ~1% from the Key Project

Proved

HubbleTension.lmc_deb_distance

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

cosmologyhubble-constant

(i) For every modulus $\mu$ , an increase by $\sqrt{0.004^2+0.026^2}$ mag increases the distance by a relative amount in $[0.0115, 0.0125)$ ( $1.2\%$ ). (ii) The Key Project LMC distance (modulus $18.5$ ) exceeds the eclipsing-binary distance (modulus $18.477$ ) by a relative amount in $[0.005, 0.015)$ ( $\sim1\%$ ).

Preamble

import Mathlib
import Definitions.Def_HubbleTension_Defs

Formal statement

namespace HubbleTension

theorem lmc_deb_distance (μ : ℝ) :
    (0.0115 ≤ (distanceFromModulus (μ + quadSum 0.004 0.026) - distanceFromModulus μ) /
        distanceFromModulus μ ∧
      (distanceFromModulus (μ + quadSum 0.004 0.026) - distanceFromModulus μ) /
        distanceFromModulus μ < 0.0125) ∧
    (0.005 ≤ (distanceFromModulus 18.5 - distanceFromModulus 18.477) / distanceFromModulus 18.477 ∧
      (distanceFromModulus 18.5 - distanceFromModulus 18.477) / distanceFromModulus 18.477
        < 0.015) := by sorry

end HubbleTension

Source

W. L. Freedman and B. F. Madore, Progress in Direct Measurements of the Hubble Constant, JCAP (2023), arXiv:2309.05618v2, https://arxiv.org/abs/2309.05618, §5.1, p. 9

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph