The reviewed record of science sign in
Pith
module module low

IndisputableMonolith.Gravity.HubbleTension

show as:
view Lean formalization →

The Gravity.HubbleTension module supplies RS/ILG definitions for late-time H₀ in km/s/Mpc together with tension metrics and sigma values. Cosmologists examining the Hubble tension cite these to contrast local and CMB measurements. It is a definitions-only module drawing on the RS time quantum from Constants.

claim$H_{0,ILG}$, $H_{0,ILG_\sigma}$, $H_{0,CMB}$, $\Delta H_0$, tension_metric, and $\sigma_{8,ILG}$ as the RS/ILG late-time Hubble constant predictions and related quantities.

background

The module resides in the Gravity domain of Recognition Science and imports Mathlib plus IndisputableMonolith.Constants. The upstream Constants module defines the fundamental RS time quantum τ₀ = 1 tick. Definitions here translate RS parameters into observable H₀ values for late-time cosmology.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the H₀ predictions that feed Hubble tension analysis in the Recognition Science framework. It connects RS landmarks (T0-T8, phi-ladder) to cosmological observables, providing a path to resolve the tension via ILG.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)