Prove2Me

Distance modulus and distance are inverse

Proved
HubbleTension.distanceModulus_inverse

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

cosmologyhubble-constant

For every real μ\mu, the distance modulus of the distance 10μ/5+110^{\mu/5+1} pc equals μ\mu; and for every distance d>0d>0 (in parsecs), 10μ(d)/5+1=d10^{\mu(d)/5+1}=d where μ(d)=5log⁡10(d/10)\mu(d)=5\log_{10}(d/10).

Preamble
import Mathlib
import Definitions.Def_HubbleTension_Defs
Formal statement
namespace HubbleTension

theorem distanceModulus_inverse :
    (∀ μ : ℝ, distanceModulus (distanceFromModulus μ) = μ) ∧
    (∀ d : ℝ, 0 < d → distanceFromModulus (distanceModulus d) = d) := 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, §5 (distance moduli used throughout; standard convention mu = 5 log10(d / 10 pc))
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