module module high

`IndisputableMonolith.Gravity.HubbleTension`

The Gravity.HubbleTension module supplies RS/ILG numerical predictions for late-time H0 in km/s/Mpc. Cosmologists comparing the Hubble tension would reference these values against CMB and local observations. It consists of definitions for H0_ILG, its sigma, delta_H0, tension_metric, and related quantities, with no internal proofs.

claimDefines $H_0^{ILG}$, $H_0^{ILG}_sigma$, $H_0^{CMB}$, $delta_H0$, the tension metric, and sound-horizon preservation quantities in RS-native units.

background

This module operates in the Gravity domain of Recognition Science and imports the fundamental time quantum tau_0 = 1 tick from IndisputableMonolith.Constants. It introduces ILG-specific predictions for the Hubble constant at late times, including uncertainty estimates, comparison to CMB values, delta_H0, and a tension metric. The module also addresses sound horizon preservation and sigma_8_ILG.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module provides the ILG Hubble constant predictions that feed into larger Recognition Science cosmology calculations. It addresses the Hubble tension by supplying RS-derived values that reduce apparent discrepancies with CMB data. Downstream results would use these to quantify tension metrics in the phi-based framework.

scope and limits

Does not derive the ILG model from first principles.
Does not integrate with full Friedmann equations.
Does not predict early-universe parameters beyond sound horizon.
Does not include observational data fitting.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (19)

def H0_ILG L27
def H0_ILG_sigma L30
def H0_CMB L33
def H0_CMB_sigma L36
def delta_H0 L39
theorem delta_H0_value L41
theorem delta_H0_positive L44
def tension_metric L52
theorem ilg_reduces_tension L56
def sound_horizon_preserved L75
theorem sound_horizon_preservation L79
def sigma_8_ILG L85
def S_8_ILG L88
def delta_chi2_improvement L91
theorem chi2_improvement_significant L93
def A_L_eff_ILG L97
theorem A_L_near_unity L99
structure HubbleTensionCert L104
theorem hubble_tension_cert L111