Hubble's law under a distance-modulus shift

Proved

HubbleTension.hubbleConstant_modulus_shift

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

cosmologyhubble-constant

For a fixed recession velocity $v$ , replacing a distance modulus $\mu$ by $\mu+\Delta$ multiplies the Hubble constant $H_0 = v/d$ inferred from Hubble's law by $10^{-\Delta/5}$ .

Preamble

import Mathlib
import Definitions.Def_HubbleTension_Defs

Formal statement

namespace HubbleTension

theorem hubbleConstant_modulus_shift (v μ Δ : ℝ) :
    hubbleConstant v (distanceFromModulus (μ + Δ)) =
      (10 : ℝ) ^ (-Δ / 5) * hubbleConstant v (distanceFromModulus μ) := 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 pp. 26-27 (Hubble's law v = H0 d, §1)

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