TRGB $H_0$ agrees with the Cepheid $H_0$ at better than $2\sigma$

Proved

HubbleTension.trgb_agrees_with_cepheid

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

cosmologyhubble-constant

The tension between the CCHP TRGB value $H_0 = 69.8 \pm 0.6\,(\mathrm{stat}) \pm 1.6\,(\mathrm{sys})$ (errors combined in quadrature) and the SH0ES Cepheid value $H_0 = 73.04 \pm 1.04$ is less than $2\sigma$ .

Preamble

import Mathlib
import Definitions.Def_HubbleTension_Defs

Formal statement

namespace HubbleTension

theorem trgb_agrees_with_cepheid :
    tension 69.8 (quadSum 0.6 1.6) 73.04 1.04 < 2 := 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, §4.1, p. 7 (SH0ES value from §3.2, p. 5)

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

TRGB H0H_0H0​ agrees with the Cepheid H0H_0H0​ at better than 2σ2\sigma2σ

TRGB $H_0$ agrees with the Cepheid $H_0$ at better than $2\sigma$