Pith. sign in
module module high

IndisputableMonolith.Cosmology.HubbleTensionBound

show as:
view Lean formalization →

Module defines the Recognition Science lower bound on the late-to-early Hubble constant ratio. Hubble tension researchers cite these results when testing RS predictions against observations. The module organizes definitions and lemmas that extend the imported Constants module.

claimThe RS-predicted lower bound on the ratio of late-time to early-time Hubble constants satisfies $H_0^{\text{late}}/H_0^{\text{early}} \geq$ bound derived from RS constants.

background

The module resides in the cosmology domain and imports the Constants module. The upstream doc-comment states: 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.' This supplies the native time scale for all subsequent bounds.

The module introduces the lower and upper bounds on the Hubble ratio together with consistency statements that apply the phi-ladder and J-cost constructions from the wider Recognition Science setting.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Hubble tension bound that supports the consistency theorems among its sibling declarations. It connects the RS constants to observational cosmology and fills the step that produces the lower bound on the late-to-early H_0 ratio.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)