HubbleTensionCert
plain-language theorem explainer
The HubbleTensionCert structure packages five conditions asserting a 3 km/s/Mpc positive shift in the inferred Hubble constant under ILG, a chi-squared improvement exceeding 10, preservation of the sound horizon, and effective lensing amplitude within 5 percent of unity. Cosmologists comparing late-time H0 inferences against CMB data would cite this certificate when documenting tension reduction in the RS/ILG framework. The structure is assembled directly from module constants delta_H0, delta_chi2_improvement, sound_horizon_preserved, and A_L_
Claim. A certificate structure asserting that the Hubble shift satisfies $0 < ΔH_0$, equals 3.0, the chi-squared improvement exceeds 10, the sound horizon remains unchanged, and the effective lensing amplitude satisfies $|A_{L, eff, ILG} - 1| < 0.05$.
background
The module formalizes the RS/ILG resolution of the Hubble tension by showing that the ILG kernel shifts late-time H0 inference while leaving early-universe quantities fixed. delta_H0 is defined as H0_ILG minus H0_CMB and set to 3.0; delta_chi2_improvement is set to 13.58; A_L_eff_ILG is defined as 1.03; sound_horizon_preserved is a boolean flag. Upstream certificates in Cosmology.HubbleTensionBound and HubbleTensionFromBIT encode band constraints and J-cost conditions that this structure complements.
proof idea
Structure definition that directly references the five module-level constants and lemmas. No tactics or reductions are applied; each field is populated by name from delta_H0, delta_chi2_improvement, sound_horizon_preserved, and A_L_eff_ILG.
why it matters
This certificate is instantiated by downstream hubbleTensionCert definitions in Cosmology.HubbleTensionBound, HubbleTensionFromBIT, and HubbleTensionPipelineFromZAging. It supplies the Gravity-specific numerical content for the Hubble-tension paper claim that ILG reduces tension from roughly 4σ to 1σ while preserving the sound horizon. It links to the RS framework's late-time modifications and touches the open question of stability under phi-ladder parameter variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.