Prove2Me

Abstract (2) — relative uncertainty 1.1%1.1\% (baseline) and 0.9%0.9\% (all estimators)

Proved
LocalDistanceNetwork.abstract_relative_uncertainty

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

cosmologynumerical-verificationstatistics

Using the values of Table 4 of the paper, the baseline solution V00 (H0=73.499±0.809 km s−1 Mpc−1H_0=73.499\pm0.809\ \mathrm{km\,s^{-1}\,Mpc^{-1}}) and the "everything available" solution V99 (H0=73.994±0.697 km s−1 Mpc−1H_0=73.994\pm0.697\ \mathrm{km\,s^{-1}\,Mpc^{-1}}) have relative uncertainties that round to 1.1%1.1\% and 0.9%0.9\% respectively:

1.05%≤0.80973.499<1.15%,0.85%≤0.69773.994<0.95%.1.05\%\le\frac{0.809}{73.499}<1.15\%,\qquad 0.85\%\le\frac{0.697}{73.994}<0.95\%.

This checks the arithmetic behind item (2) of the abstract: "A covariance-weighted combination yields a relative uncertainty of 1.1% (baseline) or 0.9% (all estimators)".

Preamble
import Mathlib
Formal statement
namespace LocalDistanceNetwork
theorem abstract_relative_uncertainty :
    (0.0105 : ℝ) ≤ 0.809 / 73.499 ∧ (0.809 : ℝ) / 73.499 < 0.0115 ∧
    (0.0085 : ℝ) ≤ 0.697 / 73.994 ∧ (0.697 : ℝ) / 73.994 < 0.0095 := 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