Prove2Me

±0.033\pm0.033 mag is a 1.5%1.5\% distance measurement

Proved
HubbleTension.modulus_error_percent

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

cosmologyhubble-constant

For every distance modulus μ\mu, increasing μ\mu by 0.0330.033 mag increases the distance by a relative amount rr with 0.0145≤r<0.01550.0145 \le r < 0.0155, i.e. 1.5%1.5\% to the quoted precision.

Preamble
import Mathlib
import Definitions.Def_HubbleTension_Defs
Formal statement
namespace HubbleTension

theorem modulus_error_percent (μ : ℝ) :
    0.0145 ≤ (distanceFromModulus (μ + 0.033) - distanceFromModulus μ) / distanceFromModulus μ ∧
    (distanceFromModulus (μ + 0.033) - distanceFromModulus μ) / distanceFromModulus μ < 0.0155 := 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.3, p. 10
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