cpl_sum_rule
plain-language theorem explainer
On the CPL thawing line the dark-energy parameters obey the exact sum rule w₀ + wₐ = −1, recovering ΛCDM in the early universe. Cosmologists matching the forced BIT redshift kernel to CPL cite this identity. The proof is a one-line ring cancellation after writing w₀ = −1 + δw₀ and wₐ = −δw₀.
Claim. For every real deviation amplitude $\delta w_0$, if $w_0 = -1 + \delta w_0$ and $w_a = -\delta w_0$, then $w_0 + w_a = -1$.
background
The module forces the shape of the BIT dark-energy kernel $K(z)$ in $w(z) = -1 + \delta w_0 \cdot K(z)$ from two premises: rung factorization (attenuation across $m+n$ $\varphi$-rungs multiplies) and single-rung balance at the unique positive fixed point $\varphi^{-1}$ of $\rho = 1/(1+\rho)$. Consequences include the rung law $\mathrm{occ}, n = \varphi^{-n}$ and the exclusion of volume or spacetime dilution in the scale-free class.
The forced kernel is identified with the Chevallier–Polarski–Linder (CPL) form $w(z) = w_0 + w_a, z/(1+z)$ on the thawing line $w_a = -(1+w_0)$. Parameterizing $w_0 = -1 + \delta w_0$ then forces $w_a = -\delta w_0$. The classical CPL sum $w_0 + w_a = -1$ is exactly the early-universe ΛCDM limit $w(z)\to -1$ as $z\to\infty$.
proof idea
One-line algebraic identity. Substitute the thawing-line parameterization into the sum and cancel: $(-1 + \delta w_0) + (-\delta w_0)$ reduces by the ring tactic to $-1$. No lemmas, hypotheses, or imports beyond basic real arithmetic are used.
why it matters
Module consequences list this identity with the CPL identification, the thawing-line placement, and the $w_0$ band: the forced kernel is exactly CPL on $w_a = -(1+w_0)$ with sum rule $w_0 + w_a = -1$ and $w_0 \in (-1,-0.88)$. It certifies that, for every admissible today-amplitude $\delta w_0$, early-time behavior is pure vacuum energy, matching the paper "The Forced Redshift Kernel." Upstream open items (the BIT aging mechanism, single-channel $d=1$ selection, the precise $\delta w_0$ interval) sit above this cancellation; the sum rule itself is unconditional once the CPL parameters are so written. Related sign control ($w(z)\ge -1$) and the retired $\Omega_\Lambda$-gap explanation live in sibling results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.