Prove2Me

Abstract (6) — baseline H0H_0 is 7.1σ7.1\sigma from Planck+Λ\LambdaCDM

Proved
LocalDistanceNetwork.abstract_tension_planck

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

cosmologynumerical-verificationstatistics

The tension between the baseline result H0=73.50±0.81 km s−1 Mpc−1H_0=73.50\pm0.81\ \mathrm{km\,s^{-1}\,Mpc^{-1}} and the early-Universe plus Λ\LambdaCDM value 67.24±0.35 km s−1 Mpc−167.24\pm0.35\ \mathrm{km\,s^{-1}\,Mpc^{-1}} rounds to 7.1σ7.1\sigma:

7.05≤∣73.50−67.24∣0.812+0.352<7.15.7.05\le\frac{|73.50-67.24|}{\sqrt{0.81^{2}+0.35^{2}}}<7.15 .

This checks the arithmetic behind the "7.1σ7.1\sigma" figure in item (6) of the abstract.

Preamble
import Mathlib
import Definitions.Def_LocalDistanceNetwork_Tension
Formal statement
namespace LocalDistanceNetwork
theorem abstract_tension_planck :
    (7.05 : ℝ) ≤ tensionSigma 73.50 0.81 67.24 0.35 ∧
    tensionSigma 73.50 0.81 67.24 0.35 < 7.15 := by sorry
end LocalDistanceNetwork
Source
H0DN Collaboration (S. Casertano et al.), The Local Distance Network: A community consensus report on the measurement of the Hubble constant at ~1% precision, A&A 708, A166 (2026), https://doi.org/10.1051/0004-6361/202557993, Abstract (p. 1), Results items (2) and (6)
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