H0_CMB
plain-language theorem explainer
CMB-inferred H₀ under standard ΛCDM is supplied as the constant 68.8. Researchers comparing early-universe CMB data to late-time measurements cite this baseline when computing the ILG-induced shift ΔH₀. The declaration is a direct numeric assignment requiring no lemmas or reduction steps.
Claim. $H_0^{CMB} = 68.8$ km s$^{-1}$ Mpc$^{-1}$, the Hubble constant inferred from CMB observations under standard ΛCDM.
background
The module formalizes the RS/ILG resolution of the Hubble tension: the ILG kernel shifts late-time H₀ inference without altering early-universe physics. Core results listed are H₀(ILG) = 71.8 ± 1.2 km/s/Mpc versus H₀(CMB) = 68.8 ± 1.1, with sound horizon r_d preserved and tension metric T dropping from ~4σ to ~1σ. H0_CMB supplies the fixed early-universe anchor for the subsequent ΔH₀ and tension calculations.
proof idea
Direct numeric definition with no lemmas applied.
why it matters
This definition anchors the early-universe side of the Hubble tension comparison. It is referenced by delta_H0 to obtain ΔH₀ = 3.0 and by ilg_reduces_tension to establish |H0_ILG - H0_CMB| < 2σ. It matches the stated core result H₀(CMB) = 68.8 ± 1.1 in the Hubble-Tension paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.