S_8_ILG
plain-language theorem explainer
RS supplies the numerical value 0.798 for the structure growth parameter S_8 under the ILG model. Cosmologists comparing CMB and late-time surveys cite this constant when quantifying the reduction in Hubble tension. The definition is a direct assignment of sigma_8 times the square root of Omega_m over 0.3 taken from the ILG calculation.
Claim. $S_8 = 0.798$, where $S_8 = sigma_8 sqrt(Omega_m / 0.3)$.
background
The module formalizes the RS/ILG resolution of the Hubble tension: the ILG kernel shifts late-time H_0 inference without altering early-universe physics such as the sound horizon. In this setting S_8 is the standard combination sigma_8 times the square root of Omega_m normalized to 0.3, and the module records the ILG value 0.798 when sigma_8 equals 0.824. The upstream theorem from PrimitiveDistinction.from converts seven independent axioms into four structural conditions plus three definitional facts that underwrite all subsequent ILG derivations.
proof idea
The declaration is a direct numerical definition that assigns the precomputed RS value for S_8 under ILG.
why it matters
This constant enters the tension_metric and ilg_reduces_tension calculations that demonstrate the drop from roughly 4 sigma to 1 sigma tension. It implements the RS prediction for late-time structure growth in the Hubble-Tension paper while preserving the sound horizon. The value is consistent with the phi-ladder mass formulas and the eight-tick octave structure of the underlying forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.