planckW0Sigma
plain-language theorem explainer
Defines the Planck+BAO+SNe one-sigma uncertainty on constant-w dark energy as 0.03. Cosmologists and RS verification authors cite it when checking that the RS baseline w(0)=-1 sits inside the observational band and that the φ^{-44} z-scale is below current precision. The body is a numeric constant definition.
Claim. The one-sigma uncertainty on the constant-$w$ dark-energy equation-of-state parameter from the Planck 2018 + BAO + SNe example is $\sigma_{w_0} = 0.03$.
background
This module attaches a dataset-specific likelihood-style certificate to the §7 dark-energy $w(z)$ falsifier row. The observational handle is the Planck 2018 + BAO + SNe constant-$w$ fit $w_0 = -1.03 \pm 0.03$. The RS structural target is $w_{\mathrm{RS}}(0) = -1$, from the linear structural law at zero redshift; sub-leading deviations scale as $\varphi^{-44} z$ and lie far below present $w$ precision.
The one-sigma width $\sigma_{w_0} = 0.03$ is the observational yardstick against which two residuals are measured: the absolute gap between the RS baseline and the Planck central value, and the $\varphi^{-44}$ target scale at $z \sim 1$. The certificate is a constant-$w$ consistency and non-sensitivity test, not a confirmation of the full dynamic RS $w(z)$.
proof idea
Pure definition: the real constant $0.03$ is introduced as the quoted Planck+BAO+SNe one-sigma uncertainty. No lemmas or tactics; downstream positivity and comparison theorems unfold this name and discharge the arithmetic by norm_num.
why it matters
This constant is the observational sigma that makes the dark-energy likelihood certificate honest. It feeds planckW0Sigma_pos (strict positivity), darkEnergyW_residual_le_one_sigma (RS $w(0)=-1$ lies within one sigma of the Planck central value; residual equals the quoted sigma), and darkEnergyW_sigma_gt_rs_z1_target (the $\varphi^{-44}$ z-scale sits below current precision). Those facts assemble into DarkEnergyWPlanckLikelihoodCert and the one-statement theorem dark_energy_w_planck_likelihood_one_statement, which also records that the §7 attachment remains marked not currently sensitive. In the broader RS verification stack this is a structural closure item (0 sorry, 0 new RS axioms), not a dynamical confirmation of $w(z)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.