OnThawingLine
plain-language theorem explainer
Defines the CPL thawing line as the relation w_a = -(1 + w_0) between the two dark-energy equation-of-state parameters. Cosmologists comparing RS predictions to DESI/Euclid CPL fits cite this predicate. It is a one-line propositional abbreviation, not a proved statement.
Claim. A pair $(w_0, w_a)$ of real CPL parameters lies on the thawing line when $w_a = -(1 + w_0)$.
background
The module forces the BIT dark-energy kernel $K(z)$ from rung factorization and single-rung balance at $\varphi^{-1}$. The resulting equation of state is $w(z) = -1 + \delta w_0 \cdot K(z)$ with $K(z) = 1/(1+z)$ on the physical branch.
In the Chevallier–Polarski–Linder (CPL) parametrization one writes $w(z) = w_0 + w_a, z/(1+z)$. Matching the forced kernel against that two-parameter family yields a one-dimensional locus in the $(w_0, w_a)$ plane: the classical thawing line $w_a = -(1+w_0)$, equivalently the sum rule $w_0 + w_a = -1$.
This definition packages that locus as a proposition on a pair of reals, so later theorems can state membership cleanly.
proof idea
Pure definitional abbreviation: the body is the equality $w_a = -(1+w_0)$. No lemmas, no tactics. Downstream proofs unfold the name and finish by ring.
why it matters
Parent results are rs_on_thawing_line (every RS amplitude $\delta w_0$ lands on the line via $w_0 = -1+\delta w_0$, $w_a = -\delta w_0$) and the one-statement summary bit_kernel_shape_one_statement, which packages the forced kernel, the thawing-line membership, the $w_0$ band, and the no-phantom bound for DESI Y3+/Roman/Euclid adjudication.
In the Recognition framework this is the cosmological readout of the $\varphi$-rung dilution law (module consequences of T6 self-similarity and cost additivity). It converts the abstract kernel shape into a sharp, observationally testable CPL constraint with sum rule $w_0 + w_a = -1$ and early-universe $\Lambda$CDM recovery. The today-amplitude $\delta w_0 \in (0, J(\varphi)]$ remains open; the line itself is forced once the kernel is.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.