rsW1DeviationTarget_pos
plain-language theorem explainer
The RS unit-redshift dark-energy deviation target is a strictly positive real. Builders of the Planck+BAO+SNe constant-w likelihood certificate need this positivity side-condition on the φ^{-44} scale. The proof unfolds the numeric attachment definition and closes the inequality by norm_num on concrete rationals.
Claim. The Recognition Science dark-energy deviation target at unit redshift is positive: $0 < \delta_{w,1}^{\mathrm{RS}}$, where $\delta_{w,1}^{\mathrm{RS}}$ is the structural $\varphi^{-44}$ scale used for the $z=1$ sub-leading correction in the constant-$w$ Planck/BAO/SNe attachment.
background
This module attaches a dataset-specific likelihood-style certificate to the §7 dark-energy $w(z)$ falsifier row. The external handle is the Planck 2018 + BAO + SNe constant-$w$ example $w_0 = -1.03 \pm 0.03$. On the RS side, the structural baseline is $w_{\mathrm{RS}}(0) = -1$ from the linear-at-zero theorem in DarkEnergyWofZStructural; corrections away from $z=0$ are suppressed by a $\varphi^{-44} z$ factor and sit far below present $w$ precision.
The named target here is that $\varphi^{-44}$ unit-redshift scale, packaged as a concrete real in the dataset attachment. Sibling facts record the Planck central value and sigma, the RS $z=0$ baseline, and the residual of baseline against the Planck central value. The certificate then asserts three honest claims: one-sigma consistency of the baseline, that the $\varphi^{-44}$ target lies below current one-sigma precision, and that the §7 row stays marked not currently sensitive.
This is a constant-$w$ baseline consistency and non-sensitivity test, not a confirmation of the full dynamic RS $w(z)$.
proof idea
Term-mode computational positivity. Unfold the deviation-target definition together with the dark-energy dataset attachment (so the target becomes an explicit numeric expression built from the $\varphi^{-44}$ scale and attachment constants), then apply norm_num to discharge $0 < \cdots$ on that concrete real. No lemmas beyond unfolding and numeric normalization are required.
why it matters
Feeds the packaged certificate darkEnergyWPlanckLikelihoodCert as the target_pos field, alongside sigma positivity, residual $\le$ one sigma, non-sensitivity of the $\varphi^{-44}$ scale relative to Planck sigma, and the dataset attachment status. Without this inequality the certificate structure cannot be inhabited.
In the broader RS verification layer this closes one of the three honest facts advertised by the module: the structural $z$-scale target is a well-formed positive quantity sitting under present $w$ precision. It supports the upgrade of the §7 dark-energy falsifier row from a bare structural claim to a dataset-linked likelihood-style certificate, while keeping the scope limited to constant-$w$ baseline consistency. Landmark contact is the RS $w_{\mathrm{RS}}(0)=-1$ baseline and the $\varphi$-ladder suppression of higher-order corrections; no T0–T8 forcing step is reopened here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.