Pith. sign in
module module high

IndisputableMonolith.Cosmology.CosmicZHistory

show as:
view Lean formalization →

Defines the BIT dark-energy equation of state and the linear cosmic Z-history that drives it: w(z)=-1+δw₀·Z(z)/Z_today. Cosmologists working the RS dark-energy plan cite it for the kernel, deviation, and monotone linear accumulator. The module builds the objects algebraically from the cost layer and proves the shape-reduction identities that force the canonical kernel.

claimUnder the BIT kernel the dark-energy equation of state is $w(z)=-1+\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$, where $Z$ is a positive, antitone linear accumulator normalized so $Z(\mathrm{today})$ is the present value, and $\delta w_0$ is the present deviation from $-1$.

background

Recognition Science cosmology treats dark energy as a residual cost defect on the cosmic ledger. The cost layer supplies the J-functional and related defect measures; Constants supplies the RS tick $\tau_0$. This module packages those ingredients into a BIT kernel: a shape for how the residual deviation from $w=-1$ accumulates with redshift.

The central objects are a bit kernel, a bit deviation $\delta w(z)$, and a linear history $Z(z)$. The deviation is required to factor as a constant present amplitude times the normalized history $Z(z)/Z_{\mathrm{today}}$. Positivity and antitonicity of $Z$ encode that the residual is larger in the past and relaxes toward today.

The local setting is the dark-energy plan inside RS cosmology: close the last free shape in $w(z)$ so that later scale-law modules can treat only amplitudes and overall normalizations.

proof idea

Definition-heavy module with supporting lemmas rather than a single top theorem. It introduces the BIT kernel and bit deviation, proves the deviation equals the normalized linear history times today's amplitude, and records the early-time and today specializations. A linear accumulator $Z$ is defined and shown positive and antitone, with an explicit today value. Shape-reduction and linear-accumulation lemmas then force that any history obeying the linear accumulation law must be the canonical kernel, closing the shape freedom.

why it matters in Recognition Science

Feeds CosmicZScaleLaw, which tightens the last shape residue in the dark-energy plan by quoting that, under the BIT kernel, $\delta w(z)=\delta w_0\cdot Z(z)/Z_{\mathrm{today}}$. Without this factorization the scale law would still carry an arbitrary redshift shape. In the broader RS chain the module sits downstream of the cost/J layer and the RS tick, and upstream of amplitude and observational matching for $w(z)$. It does not itself fix $\delta w_0$ or connect to the eight-tick or $D=3$ forcing steps; those remain in the foundation and constants layers.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)