H0_ILG
plain-language theorem explainer
The declaration supplies the numerical value of the late-time Hubble constant predicted by the ILG kernel in Recognition Science. Cosmologists working on the Hubble tension would cite this constant when comparing late-time and CMB inferences. It is introduced as a direct definition with no computational steps.
Claim. The ILG-predicted late-time Hubble constant is $H_0^{ILG} = 71.8$ km s^{-1} Mpc^{-1}.
background
The Hubble Tension module formalizes the RS/ILG resolution of the Hubble tension: the ILG kernel shifts late-time H0 inference without altering early-universe physics. The value H0_ILG is the central prediction for late-time measurements. Upstream, the Uncertainty inductive type from RSNative.Core supplies the reporting semantics for the associated 1.2 km/s/Mpc error bar via its sigma constructor.
proof idea
This is a direct definition that assigns the real number 71.8 to H0_ILG. No lemmas or tactics are applied.
why it matters
This constant anchors the ILG resolution of the Hubble tension. It is used to define the shift delta_H0 and to prove that the tension metric drops below 2 sigma in ilg_reduces_tension. In the Recognition Science framework it embodies the late-time modification that preserves the sound horizon while moving H0 from the CMB value of 68.8 to 71.8, reducing the discrepancy from roughly 4 sigma to 1 sigma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.