Prove2Me

Eq. (8): the H0(z)H_0(z) diagnostic is constant iff H(z)H(z) is flat ΛCDM

Proved
HuWang2023.h0Diagnostic_const_iff

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

cosmology

Let Ωm0≥0\Omega_{m0}\ge0, H0∈RH_0\in\mathbb R and let H:R→RH:\mathbb R\to\mathbb R be any expansion history. The H0H_0 diagnostic of Eq. (8),

H0(z)=H(z)1−Ωm0+Ωm0(1+z)3,H_0(z) = \frac{H(z)}{\sqrt{1-\Omega_{m0}+\Omega_{m0}(1+z)^3}},

equals the constant H0H_0 for all z≥0z\ge0 if and only if

H(z)=H0Ωm0(1+z)3+1−Ωm0for all z≥0,H(z) = H_0\sqrt{\Omega_{m0}(1+z)^3 + 1-\Omega_{m0}} \quad\text{for all } z\ge0,

that is, if and only if HH is the expansion history of flat ΛCDM with parameters (H0,Ωm0)(H_0, \Omega_{m0}).

This is why a redshift dependence ("running") of the diagnostic H0(z)H_0(z) signals a deviation from flat ΛCDM, as used in Section 5.

Preamble
import Mathlib
import Definitions.Def_HuWang2023_HubbleTension_Defs
Formal statement
namespace HuWang2023

theorem h0Diagnostic_const_iff (Ωm0 H0 : ℝ) (H : ℝ → ℝ)
    (hΩm0 : 0 ≤ Ωm0) :
    (∀ z, 0 ≤ z → h0Diagnostic Ωm0 H z = H0) ↔ (∀ z, 0 ≤ z → H z = flatHubble H0 Ωm0 z) := by sorry

end HuWang2023
Source
Jian-Ping Hu and Fa-Yin Wang, *Hubble Tension: The Evidence of New Physics*, Universe 2023, 9(2), 94, https://doi.org/10.3390/universe9020094, Section 5, p. 14, Eq. (8) and the sentence following it
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