NGC 4258: modulus 29.397 is 7.6 Mpc
ProvedHubbleTension.ngc4258_distancecosmologyhubble-constant
The distance pc corresponding to the maser distance modulus of NGC 4258 lies in pc, i.e. it is Mpc to the quoted precision.
Preamble
import Mathlib import Definitions.Def_HubbleTension_Defs
Formal statement
namespace HubbleTension
theorem ngc4258_distance :
7.55e6 ≤ distanceFromModulus 29.397 ∧ distanceFromModulus 29.397 < 7.65e6 := by sorry
end HubbleTensionSource
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.