planckOmegaLambdaSigma_pos
plain-language theorem explainer
The Planck 2018 one-sigma error bar on ΩΛ is strictly positive. Cosmology and verification authors cite it when assembling the ΩΛ likelihood-style certificate and when lifting positivity to the two-sigma width. The proof unfolds the sigma definition to the numeric Planck error 0.0056 and closes by norm_num.
Claim. The Planck 2018 one-sigma uncertainty on $\Omega_\Lambda$ satisfies $0 < \sigma_{\Omega_\Lambda}^{\mathrm{Planck}}$, where that uncertainty is the fixed real $0.0056$.
background
This module attaches a dataset-specific likelihood-style Lean certificate to the §7 ΩΛ falsifier-register row. The RS prediction is $\omega_\lambda = 11/16 - \alpha/\pi$, forced into the open interval $(0.683, 0.686)$, and checked for two-sigma consistency against Planck 2018 TT,TE,EE+lowE+lensing ($\Omega_\Lambda = 0.6889 \pm 0.0056$). The module states this is a consistency test, not empirical confirmation.
The one-sigma width used here is defined as planckOmegaLambdaSigma, equal by definition to the cosmology constant omega_lambda_planck_err := 0.0056 ("Planck 2018 error bar (1σ)"). Downstream residual and interval lemmas compare the RS central prediction to that Planck central value against multiples of this width.
proof idea
Term-mode proof by unfolding. Expand planckOmegaLambdaSigma to omega_lambda_planck_err, then expand that definition to the literal real $0.0056$. A single norm_num discharges $0 < 0.0056$. No lemmas beyond definitional equality are required.
why it matters
Positivity of the one-sigma bar is a structural precondition for the likelihood certificate. It is a field of omegaLambdaPlanckLikelihoodCert (sigma_pos := planckOmegaLambdaSigma_pos) and is the only non-trivial input to planckOmegaLambdaTwoSigma_pos, which multiplies the same width by two. Without a proved positive sigma, the two-sigma residual comparison and the interval-form certificate cannot be inhabited. In the Recognition verification stack this closes the numeric side of the ΩΛ Planck attachment (module status: structural theorem, zero sorry, zero new RS axioms), sitting under the broader falsifier-register consistency program rather than under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.