Prove2Me

A modulus +0.45+0.45 mag farther lowers H0H_0

Proved
HubbleTension.jwst_crowding_lowers_H0

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

cosmologyhubble-constant

For every positive recession velocity vv and every distance modulus μ\mu, the Hubble constant inferred at modulus μ+0.45\mu+0.45 is strictly smaller than the one inferred at μ\mu.

Preamble
import Mathlib
import Definitions.Def_HubbleTension_Defs
Formal statement
namespace HubbleTension

theorem jwst_crowding_lowers_H0 (v μ : ℝ) (hv : 0 < v) :
    hubbleConstant v (distanceFromModulus (μ + 0.45)) < 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, p. 26
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