planckW0Sigma_pos
plain-language theorem explainer
The Planck+BAO+SNe constant-w one-sigma uncertainty is strictly positive. Anyone assembling the dark-energy w0 likelihood certificate needs this positivity side-condition. The proof unfolds the numeric definition 0.03 and discharges the inequality by norm_num.
Claim. The Planck+BAO+SNe constant-$w$ one-sigma uncertainty satisfies $0 < \sigma_{w_0}^{\mathrm{Planck}}$, where $\sigma_{w_0}^{\mathrm{Planck}} = 0.03$.
background
This module attaches a dataset-specific likelihood-style certificate to the §7 dark-energy $w(z)$ falsifier row. The quoted Planck 2018 + BAO + SNe constant-$w$ example is $w_0 = -1.03 \pm 0.03$. The RS structural baseline is $w_{\mathrm{RS}}(0) = -1$, from the structural $w(z)$ development; sub-leading redshift deviations scale as $\varphi^{-44} z$ and sit far below present $w$ precision.
The constant planckW0Sigma is the one-sigma half-width $0.03$ on that constant-$w$ fit. Positivity of the uncertainty is a trivial but required field of the certificate record: residuals and sensitivity comparisons are only meaningful when $\sigma > 0$.
proof idea
One-line tactic proof: unfold the definition planckW0Sigma (which is the literal real $0.03$), then norm_num closes $0 < 0.03$. No lemmas beyond the definition are required.
why it matters
Feeds the sigma_pos field of darkEnergyWPlanckLikelihoodCert, the module's top-level certificate packing the three honest facts: RS baseline within one sigma of the Planck/BAO/SNe central value, the $\varphi^{-44}$ $z$-scale target below current one-sigma precision, and the §7 row still marked not currently sensitive. Without $\sigma > 0$, the residual and sensitivity comparisons in that record are ill-typed. This is bookkeeping for a constant-$w$ consistency / non-sensitivity test, not a dynamical confirmation of RS $w(z)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.