H_late
plain-language theorem explainer
Late-universe Hubble constant fixed at the representative 2022 value 73.04 (SH0ES-type). Cosmologists and RS verifiers cite it as the late anchor when forming the tension metric or checking the predicted late/early ratio. The declaration is a pure numeric definition with no proof obligations.
Claim. The representative late-time Hubble measurement is the real number $H_{\mathrm{late}} = 73.04$.
background
This module is a pure data store for Hubble-tension inputs and the Planck $\Omega_\Lambda$ figure. Values are meant to be updated when new releases appear; nothing here derives a constant from first principles.
$H_{\mathrm{late}}$ is the late-universe (local distance-ladder) Hubble number used opposite the early/CMB anchor. Its sibling $H_{\mathrm{early}}$ supplies the other side of the comparison. Downstream, the tension metric is $T = |\Delta H_0|/\sqrt{\sigma_{\mathrm{late}}^2+\sigma_{\mathrm{CMB}}^2}$, and the RS prediction module freezes the ratio target at $13/12$.
proof idea
Definitional binding only: the real constant is set equal to $73.04$. No lemmas, tactics, or hypotheses.
why it matters
Supplies the late anchor for three consumers. tension_metric builds $T = |H_{\mathrm{late}}-H_{\mathrm{early}}|/\sqrt{\sigma^2_{\mathrm{late}}+\sigma^2_{\mathrm{early}}}$, the quantity that is $\sim 4$–$5\sigma$ under plain $\Lambda$CDM and $\sim 1\sigma$ under ILG. hubble_ratio packages the RS claim $H_{\mathrm{late}}/H_{\mathrm{early}}=13/12$. The arithmetic test hubble_ratio_passes_rel_0p05pct checks that $H_{\mathrm{early}}\cdot(13/12)$ recovers this $H_{\mathrm{late}}$ to relative error $<5\times 10^{-4}$. In the broader RS ledger this is verification scaffolding, not a forcing-chain step (T0–T8); it lets the preregistered Hubble prediction be scored against published numbers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.