Prove2Me

Abstract (6) — baseline H0H_0 is 5.0σ5.0\sigma from BBN+BAO (DESI DR2)

Proved
LocalDistanceNetwork.abstract_tension_desi

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 BBN+BAO value within flat Λ\LambdaCDM from DESI DR2, 68.51±0.58 km s−1 Mpc−168.51\pm0.58\ \mathrm{km\,s^{-1}\,Mpc^{-1}}, rounds to 5.0σ5.0\sigma:

4.95≤∣73.50−68.51∣0.812+0.582<5.05.4.95\le\frac{|73.50-68.51|}{\sqrt{0.81^{2}+0.58^{2}}}<5.05 .

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

Preamble
import Mathlib
import Definitions.Def_LocalDistanceNetwork_Tension
Formal statement
namespace LocalDistanceNetwork
theorem abstract_tension_desi :
    (4.95 : ℝ) ≤ tensionSigma 73.50 0.81 68.51 0.58 ∧
    tensionSigma 73.50 0.81 68.51 0.58 < 5.05 := 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