A $-0.123$ mag offset is a $6\%$ shift in $H_0$

Proved

HubbleTension.r16_r22_six_percent_shift

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

cosmologyhubble-constant

For every positive velocity $v$ and modulus $\mu$ , decreasing the distance modulus by $0.123$ mag increases the inferred Hubble constant by a relative amount $r$ with $0.055 \le r < 0.065$ , i.e. by $6\%$ to the quoted precision.

Preamble

import Mathlib
import Definitions.Def_HubbleTension_Defs

Formal statement

namespace HubbleTension

theorem r16_r22_six_percent_shift (v μ : ℝ) (hv : 0 < v) :
    0.055 ≤ hubbleConstant v (distanceFromModulus (μ - 0.123)) /
        hubbleConstant v (distanceFromModulus μ) - 1 ∧
    hubbleConstant v (distanceFromModulus (μ - 0.123)) /
        hubbleConstant v (distanceFromModulus μ) - 1 < 0.065 := 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, Summary, p. 27

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

A −0.123-0.123−0.123 mag offset is a 6%6\%6% shift in H0H_0H0​

A $-0.123$ mag offset is a $6\%$ shift in $H_0$