planckOmegaLambdaTwoSigma
plain-language theorem explainer
Two-sigma Planck 2018 tolerance on dark-energy density ΩΛ, defined as twice the reported one-sigma uncertainty. Verification and cosmology readers cite it when checking that the RS closed-form ΩΛ sits inside the Planck band. The body is a one-line scaling of the imported Planck error constant.
Claim. Let $\sigma_{\Omega_\Lambda}$ be the Planck 2018 one-sigma uncertainty on $\Omega_\Lambda$. The two-sigma tolerance is defined by $2\sigma_{\Omega_\Lambda}$.
background
This module attaches a likelihood-style Lean certificate to the §7 ΩΛ falsifier-register row. The RS prediction is the closed form $\omega_\lambda = 11/16 - \alpha/\pi$ from Cosmology.OmegaLambdaDerivation, already known to lie in $(0.683, 0.686)$. The external dataset is Planck 2018 TT,TE,EE+lowE+lensing with central value $\Omega_\Lambda = 0.6889 \pm 0.0056$.
The one-sigma width is the upstream constant planckOmegaLambdaSigma, equal to the imported Planck error omega_lambda_planck_err. The two-sigma width is the natural comparison scale for the residual test that the module packages as a structural certificate (zero sorry, no new RS axioms). The module itself stresses that this is a consistency test, not empirical confirmation.
proof idea
One-line definition: twice the Planck one-sigma uncertainty. No tactics or lemmas; pure arithmetic scaling of the upstream constant.
why it matters
Supplies the comparison threshold for the residual inequality (RS residual strictly less than two-sigma), the open-interval form of that statement, positivity of the two-sigma width, the master certificate structure, and the one-statement likelihood attachment theorem. Those parents close the Planck-likelihood row of the ΩΛ falsifier register: the RS interval is currently sensitive at two-sigma consistency with Planck 2018. Landmark context is the derived cosmological constant density from the Recognition chain, not a free fit parameter; the certificate only records agreement with the external band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.