rsW1DeviationTarget
plain-language theorem explainer
RS structural deviation target at redshift z=1, taken from the dark-energy dataset attachment as the φ^{-44} scale. Cosmologists citing the Planck/BAO/SNe w0 likelihood certificate use it to show that sub-leading RS w(z) drift sits below present one-sigma precision. The definition is a one-line alias of the attachment's target-scale field.
Claim. The RS structural deviation target at redshift $z=1$ is the positive real target scale recorded on the dark-energy $w$ dataset attachment (the $\varphi^{-44}$ $z$-scale used for non-sensitivity checks against Planck+BAO+SNe constant-$w$ precision).
background
This module attaches a likelihood-style certificate to the §7 dark-energy $w(z)$ falsifier row using the Planck 2018 + BAO + SNe constant-$w$ example $w_0 = -1.03 \pm 0.03$. The RS baseline is $w_{\mathrm{RS}}(0) = -1$ from the structural $w(z)$ development; deviations away from $z=0$ are suppressed by a $\varphi^{-44} z$ factor and are far below current $w$ precision.
The dataset attachment (darkEnergyWAttachment) packages sensitivity flags, a residual against the RS baseline, and a structural target scale. This definition simply names that target scale as the RS $z=1$ deviation target. Downstream positivity and comparison lemmas unfold it and discharge numeric inequalities by norm_num.
The certificate is a constant-$w$ baseline consistency / non-sensitivity test, not a confirmation of the full dynamic RS $w(z)$ shape.
proof idea
Pure definition: a one-line abbreviation equal to darkEnergyWAttachment.rsTargetScale. No proof obligations. Downstream lemmas (rsW1DeviationTarget_pos, darkEnergyW_sigma_gt_rs_z1_target) unfold this alias together with the attachment and the Planck sigma constant, then close the comparisons by numeric normalization.
why it matters
Gives a named handle for the $\varphi^{-44}$ $z$-scale that the module's three honest facts rely on. It feeds rsW1DeviationTarget_pos (strict positivity), darkEnergyW_sigma_gt_rs_z1_target (target strictly below Planck one-sigma $w$ precision), the certificate structure DarkEnergyWPlanckLikelihoodCert (field target_pos), and the one-statement theorem dark_energy_w_planck_likelihood_one_statement.
In the Recognition framework this closes the structural non-sensitivity half of the dark-energy $w$ verification row: RS predicts $w(0)=-1$ with higher-order drift far below present data, so the §7 attachment stays marked not currently sensitive. It does not touch the forcing chain (T0–T8) or the RCL; it is a verification-layer numeric bridge between cosmology structure and the falsifier register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.