Hubble tension: $5\sigma$ , below $3\sigma$ at $\pm1.5$ , $2\sigma$ at $\pm2.0$

Proved

HubbleTension.hubble_tension_section10

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

cosmologyhubble-constant

With $\mathrm{tension}(a,\sigma_a,b,\sigma_b)=|a-b|/\sqrt{\sigma_a^2+\sigma_b^2}$ and the Planck value $67.4 \pm 0.5$ : (i) the SH0ES value $73.04 \pm 1.04$ is in tension $t$ with $4.5 \le t < 5.5$ (a $5\sigma$ tension); (ii) a local value $72.0 \pm 1.5$ is in tension less than $3\sigma$ ; (iii) a local value $72.0 \pm 2.0$ is in tension $t$ with $1.5 \le t < 2.5$ (a $2\sigma$ tension).

Preamble

import Mathlib
import Definitions.Def_HubbleTension_Defs

Formal statement

namespace HubbleTension

theorem hubble_tension_section10 :
    (4.5 ≤ tension 73.04 1.04 67.4 0.5 ∧ tension 73.04 1.04 67.4 0.5 < 5.5) ∧
    tension 72.0 1.5 67.4 0.5 < 3 ∧
    (1.5 ≤ tension 72.0 2.0 67.4 0.5 ∧ tension 72.0 2.0 67.4 0.5 < 2.5) := 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, §10, p. 25 (SH0ES value from §3.2, p. 5; Planck value from §1, p. 1)

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

Hubble tension: 5σ5\sigma5σ, below 3σ3\sigma3σ at ±1.5\pm1.5±1.5, 2σ2\sigma2σ at ±2.0\pm2.0±2.0

Hubble tension: $5\sigma$ , below $3\sigma$ at $\pm1.5$ , $2\sigma$ at $\pm2.0$