Prove2Me

Sect. 5.2.4 — V99 is 8.7σ8.7\sigma and V99a is 8.1σ8.1\sigma from Planck+Λ\LambdaCDM

Proved
LocalDistanceNetwork.everything_tensions

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

cosmologynumerical-verificationstatistics

With the Table 4 values of the "everything available" solution V99 (73.994±0.69773.994\pm0.697) and of V99A, everything except the Tully–Fisher relation (73.656±0.71373.656\pm0.713), the tensions with the Planck+Λ\LambdaCDM value 67.24±0.3567.24\pm0.35 (all in km s−1 Mpc−1\mathrm{km\,s^{-1}\,Mpc^{-1}}) round to 8.7σ8.7\sigma and 8.1σ8.1\sigma:

8.65≤∣73.994−67.24∣0.6972+0.352<8.75,8.05≤∣73.656−67.24∣0.7132+0.352<8.15.8.65\le\frac{|73.994-67.24|}{\sqrt{0.697^{2}+0.35^{2}}}<8.75,\qquad 8.05\le\frac{|73.656-67.24|}{\sqrt{0.713^{2}+0.35^{2}}}<8.15 .

This checks the arithmetic behind the "8.7σ8.7\sigma" and "8.1σ8.1\sigma" figures of Sect. 5.2.4.

Formalization Note The unrounded Table 4 values are used. With the rounded text values 73.99±0.7073.99\pm0.70 the V99 tension would be about 8.62σ8.62\sigma, which rounds to 8.68.6 rather than the quoted 8.78.7.

Preamble
import Mathlib
import Definitions.Def_LocalDistanceNetwork_Tension
Formal statement
namespace LocalDistanceNetwork
theorem everything_tensions :
    ((8.65 : ℝ) ≤ tensionSigma 73.994 0.697 67.24 0.35 ∧
      tensionSigma 73.994 0.697 67.24 0.35 < 8.75) ∧
    ((8.05 : ℝ) ≤ tensionSigma 73.656 0.713 67.24 0.35 ∧
      tensionSigma 73.656 0.713 67.24 0.35 < 8.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, Sect. 5.2.4 (p. 17) and Table 4 (p. 9), rows V99 and V99A
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