Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.OmegaLambdaBITKernelBand

show as:
view Lean formalization →

Defines the Recognition Science cosmological constant density Λ_RS = 8φ⁵/45 and certifies that it lies in a narrow positive band suitable for Ω_Λ comparisons. Cosmologists matching RS predictions to the observed dark-energy fraction would cite the band certificate. The module is mostly definitional arithmetic on φ together with interval bounds.

claimThe RS cosmological constant density is $\Lambda_{\mathrm{RS}} = 8\varphi^5/45$, where $\varphi$ is the golden-ratio fixed point. The module records $\Lambda_{\mathrm{RS}} > 0$ and places it inside an explicit numerical band used for $\Omega_\Lambda$ kernel comparisons.

background

Recognition Science fixes the dimensionless cost $J(x) = (x+x^{-1})/2-1$ and forces $\varphi$ as the unique self-similar fixed point of the recognition composition law. Dimensionful constants are then expressed in RS-native units built from powers of $\varphi$ (e.g. $\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$).

Cosmology inherits the same ladder. The present module isolates one pure number, $\Lambda_{\mathrm{RS}} = 8\varphi^5/45$, intended as the RS prediction for the vacuum-energy density that enters $\Omega_\Lambda$. The factor $8/45$ is the BIT-kernel normalisation that converts the $\varphi^5$ scale into a density fraction comparable with late-time cosmology.

Upstream material is limited to the Constants and Cost modules, which supply $\varphi$ and the elementary algebraic identities needed to evaluate powers and clear denominators.

proof idea

The module is definition-first. $\lambda_{\mathrm{RS}}$ is introduced by the closed formula $8\varphi^5/45$. A short algebraic identity equates $\varphi^5$ to its expanded radical form so that numerical bounds can be discharged by interval arithmetic. Positivity is immediate from $\varphi>1$. The band certificate packages the resulting closed interval together with the positivity claim into a single named witness usable by downstream cosmology checks. No deep forcing-chain argument appears; the work is pure arithmetic on the already-forced constant $\varphi$.

why it matters in Recognition Science

Supplies the concrete RS value and certified band for the dark-energy density that later cosmology modules compare with observed $\Omega_\Lambda$. Without a pinned $\Lambda_{\mathrm{RS}}$ the BIT-kernel route from the eight-tick octave and $\varphi$-ladder to late-time expansion cannot be audited. The module sits at the cosmology leaf of the framework: it consumes only Constants and Cost, and currently has no recorded downstream dependents inside the mirror, so it functions as a self-contained prediction package ready for external numerical confrontation.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)