Pith. sign in
module module high

IndisputableMonolith.Cosmology.HubbleTension

show as:
view Lean formalization →

This module defines the Hubble ratio of 13/12 from Recognition Science ledger geometry applied to cosmology. It exports expressions for early and late Hubble parameters, dark energy density, and topological bounds on the ratio. Cosmologists studying the H0 discrepancy would cite these definitions to connect alpha and CKM derivations to expansion history. The module consists of assembled definitions with no internal proofs.

claim$H_{\rm late}/H_{\rm early}=13/12$, where $H_{\rm early}$ and $H_{\rm late}$ are expressed via the phi-ladder and defect geometry, $\Omega_L$ denotes the dark energy density parameter, and bounds follow from the cubic ledger.

background

The module imports the RS time quantum $\tau_0=1$ tick from Constants, the derivation of $\alpha^{-1}$ from vertex deficits of the cubic ledger Q3 via Gauss-Bonnet in AlphaDerivation, and the CKM matrix elements obtained from the same ledger geometry in CKMGeometry. These supply the microscopic inputs. The local setting is the Recognition Science forcing chain (T0-T8) extended to late-time cosmology, with the eight-tick octave and D=3 dimensions already fixed upstream.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Hubble ratio 13/12 and related expressions that feed directly into the parent theorem T-001 in HubbleTensionCertificate, which resolves the early-versus-late universe H0 discrepancy. It closes the step from alpha derivation and CKM geometry to observable cosmological parameters.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (18)