rs_on_thawing_line
plain-language theorem explainer
For every dark-energy amplitude δw₀ the RS CPL parameters sit exactly on the thawing line w_a = −(1+w_0). Cosmologists matching RS dark energy to DESI/Euclid CPL fits would cite this identity. The proof is pure algebra: unfold the thawing-line predicate and cancel.
Claim. For every real amplitude $\delta w_0$, the CPL pair $w_0 = -1 + \delta w_0$ and $w_a = -\delta w_0$ satisfies the thawing-line relation $w_a = -(1 + w_0)$.
background
The module forces the BIT dark-energy kernel from two premises: rung factorization of aging-charge attenuation across φ-rungs, and single-rung balance fixing the attenuation to φ⁻¹. The resulting equation of state is written in CPL form w(z) = w₀ + w_a z/(1+z), equivalently w(z) = −1 + δw₀ · K(z) with the forced kernel K(z) = 1/(1+z).
In that parameterization the today value is w₀ = −1 + δw₀ and the slope is w_a = −δw₀. The thawing line in the (w₀, w_a) plane is the locus w_a = −(1 + w₀); it is the classical boundary separating thawing from freezing quintessence trajectories and is exactly the CPL sum rule w₀ + w_a = −1 (early-universe ΛCDM recovery).
The predicate OnThawingLine is that equality as a Prop on a pair of reals. This lemma simply records that the RS amplitude map lands on that line for every real δw₀.
proof idea
Term-mode proof by unfolding. Expand the thawing-line predicate to the equality w_a = −(1 + w₀), substitute w₀ = −1 + δw₀ and w_a = −δw₀, and finish with ring. No external lemmas are required; the identity is −δw₀ = −(1 + (−1 + δw₀)).
why it matters
This is one of the five conjuncts packaged by bit_kernel_shape_one_statement, the module's one-statement summary: the forced BIT kernel is CPL on the thawing segment w_a = −(1+w₀) with w₀ ∈ (−1, −0.88) and no phantom crossing, to be tested by DESI Y3+ / Roman / Euclid.
Together with the companion sum-rule and w₀-band results listed in the module header, it converts the abstract rung-dilution law occ n = φ⁻ⁿ into a concrete, observationally standard CPL claim. The thawing-line landing is model-independent once the kernel is K(z) = 1/(1+z); only the open amplitude window δw₀ ∈ (0, J(φ)] remains as a hypothesis-level input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.