pith. sign in
module module high

IndisputableMonolith.Cosmology.HubbleTensionFromBIT

show as:
view Lean formalization →

The module supplies the Recognition Science formula for Hubble tension amplitude as J(φ) log(2). Cosmologists examining the early-versus-late universe discrepancy cite it for its zero-parameter prediction inside the RS framework. The module assembles this result from imported constants and cost functions as a set of definitions without theorems.

claimThe RS Hubble tension amplitude equals $J(φ) log(2)$, where $J(x) = (x + x^{-1})/2 - 1$ and $φ$ is the self-similar fixed point.

background

Recognition Science derives cosmology from the J-cost function and the forcing chain. Constants supplies the fundamental time quantum τ₀ = 1 tick. Cost supplies the J-cost machinery that obeys the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module applies these to the phi-ladder to obtain a cosmological amplitude. The module doc-comment states the central result directly: RS Hubble tension amplitude = J(φ) × log(2).

proof idea

This is a definition module, no proofs. It introduces hubbleTensionAmplitude together with supporting definitions jcost_phi_band, hubble_tension_pos, jcost_phi_pos, HubbleTensionCert and hubbleTensionCert.

why it matters in Recognition Science

The module supplies the Hubble tension amplitude to the cosmology section of the Recognition Science mirror. It connects the J-uniqueness step (T5) and phi fixed point (T6) of the forcing chain to an observable cosmological quantity. No downstream theorems are recorded, so the module functions as a leaf definition for later cosmological applications.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)