rsW0Baseline
plain-language theorem explainer
The RS structural dark-energy baseline at redshift zero equals −1. Cosmologists and verifiers cite it when attaching the Planck+BAO+SNe constant-w datum to the §7 falsifier row. It is the one-line evaluation of the linear witness profile w_RS_linear at z = 0, which is forced to −1 by construction.
Claim. The Recognition Science structural baseline for the dark-energy equation-of-state parameter at redshift zero is $w_{\mathrm{RS}}(0) := -1 + \varphi^{-44}\cdot 0 = -1$.
background
This module attaches a Planck 2018 + BAO + SNe constant-w likelihood-style certificate to the §7 dark-energy $w(z)$ falsifier. The quoted dataset handle is $w_0 = -1.03 \pm 0.03$. The RS side supplies a structural target at $z=0$ and a sub-leading slope scale $\varphi^{-44} z$ far below present $w$ precision.
The upstream profile $w_{\mathrm{RS,linear}}(z) := -1 + \varphi^{-44}\cdot z$ is documented as a generic non-$\Lambda$CDM witness, not the full RS dark-energy equation of state. Its honesty warning is explicit: at $z=0$ it matches $\Lambda$CDM exactly; at positive redshift the deviation is the tiny positive term $\varphi^{-44} z$. The present definition simply names the $z=0$ value of that profile as the RS baseline used by the residual and one-sigma checks.
proof idea
Pure definition: evaluate the upstream linear witness $w_{\mathrm{RS,linear}}$ at argument $0$. No tactics. Downstream proofs unfold this name and rewrite with $w_{\mathrm{RS,linear}}(0)=-1$ (via w_RS_linear_at_zero) before norm_num.
why it matters
Names the RS $z=0$ anchor that the residual $|w_0^{\mathrm{Planck}}-w_{\mathrm{RS}}(0)|$ and the theorem darkEnergyW_residual_le_one_sigma compare to the Planck+BAO+SNe central value and sigma. That theorem shows the residual equals the quoted $0.03$ sigma, so the baseline sits at the one-sigma boundary (non-strict). The module certificate also records that the $\varphi^{-44}$ $z$-scale target lies below current precision and that the §7 row stays marked not currently sensitive. This is constant-$w$ baseline consistency and non-sensitivity, not a confirmation of dynamic RS $w(z)$. It closes a structural verification attachment with zero sorry and no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.