NGC 4258: TRGB and maser moduli agree

Proved

HubbleTension.ngc4258_trgb_agrees_with_maser

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

cosmologyhubble-constant

The TRGB modulus $29.392 \pm 0.018 \pm 0.032$ (errors combined in quadrature) and the maser modulus $29.397 \pm 0.033$ of NGC 4258 differ by less than $0.2\sigma$ , and the corresponding distances differ by less than $1\%$ (relative to the TRGB distance).

Preamble

import Mathlib
import Definitions.Def_HubbleTension_Defs

Formal statement

namespace HubbleTension

theorem ngc4258_trgb_agrees_with_maser :
    tension 29.392 (quadSum 0.018 0.032) 29.397 0.033 < 0.2 ∧
    |distanceFromModulus 29.397 - distanceFromModulus 29.392| / distanceFromModulus 29.392
      < 0.01 := 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