Pith. sign in
def

w_CPL

definition
show as:
module
IndisputableMonolith.Cosmology.BITKernelShapeForcing
domain
Cosmology
line
219 · github
papers citing
none yet

plain-language theorem explainer

Defines the Chevallier–Polarski–Linder (CPL) dark-energy equation of state in redshift form: $w(z)=w_0+w_a\,z/(1+z)$. Cosmologists comparing RS-forced $w(z)$ to standard parametrizations cite this. The body is a one-line arithmetic definition with no proof obligations.

Claim. For real parameters $w_0$, $w_a$ and redshift $z$, the CPL equation of state is $w_{\mathrm{CPL}}(w_0,w_a,z) := w_0 + w_a \cdot \frac{z}{1+z}$.

background

The module forces the shape of the BIT dark-energy kernel $K(z)$ from two premises: rung factorization (attenuation multiplies across independent $\varphi$-rungs) and single-rung balance (one rung attenuates by $\varphi^{-1}$, the positive fixed point of $\rho=1/(1+\rho)$). The resulting occupation law is $\mathrm{occ},n=\varphi^{-n}$, which on the lattice $1+z=\varphi^n$ is $1/(1+z)$.

CPL is the standard two-parameter redshift form used in observational cosmology to expand $w(z)$ about today. In this file the RS dark-energy law is written $w_{\mathrm{RS}}(\delta w_0,z)=-1+\delta w_0\cdot K(z)$ with the forced kernel $K(z)=1/(1+z)$. Matching that expression to CPL is the content of the downstream identification theorem.

Upstream kernel families supply the candidate shapes (constant, inverse-$(1+z)$, exponential); the forcing chain selects the inverse-$(1+z)$ member.

proof idea

Pure definition: the right-hand side is the classical CPL formula. No lemmas, no tactics, no hypotheses. Downstream proofs unfold this abbreviation and simplify algebraically against $w_{\mathrm{RS}}$.

why it matters

Parent theorem w_RS_is_CPL states that the forced RS equation of state is exactly CPL with $w_0=-1+\delta w_0$ and $w_a=-\delta w_0$. That identification places RS on the thawing line $w_a=-(1+w_0)$ with sum rule $w_0+w_a=-1$, and feeds the certified band $w_0\in(-1,-0.88)$, the no-phantom bound $w(z)\ge-1$, and the retirement of the "$\Omega_\Lambda$ gap" hypothesis.

In the paper companion "The Forced Redshift Kernel," this is the bridge from the discrete rung law to the continuous observational language. It does not itself force $\delta w_0$; that amplitude remains open in $(0,J(\varphi)]$.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.