planckOmegaLambdaSigma
plain-language theorem explainer
Aliases the Planck 2018 one-sigma uncertainty on dark-energy density to the real 0.0056. Cosmologists checking the RS ΩΛ prediction against TT,TE,EE+lowE+lensing cite this as the σ scale for residual and interval tests. The body is a one-line definitional synonym of the cosmology-module error bar.
Claim. The Planck 2018 one-sigma uncertainty on $\Omega_\Lambda$ is the real number $0.0056$.
background
The module attaches a likelihood-style certificate to the §7 ΩΛ falsifier-register row. Recognition Science predicts $\omega_\lambda = 11/16 - \alpha/\pi$, confined to the open interval $(0.683, 0.686)$. Planck 2018 (TT,TE,EE+lowE+lensing) reports $\Omega_\Lambda = 0.6889 \pm 0.0056$.
Upstream, omega_lambda_planck_err is the noncomputable real $0.0056$, documented as the Planck 2018 $1\sigma$ error bar. The same cosmology source already records two-sigma consistency: the RS interval sits inside $0.6889 \pm 2\times 0.0056 = (0.6833, 0.6945)$. This definition simply re-exports that error bar under a verification-local name so residual and certificate constructions stay readable.
proof idea
Definitional one-liner: the symbol is set equal to the upstream cosmology constant omega_lambda_planck_err, whose value is the literal real $0.0056$. No tactics or lemmas are involved.
why it matters
Gives the verification layer a stable name for Planck's $1\sigma$ scale. Downstream, twice this quantity is the two-sigma tolerance; the absolute residual between the RS prediction and the Planck central value is required to be strictly smaller than that tolerance; positivity of the sigma feeds the master structure OmegaLambdaPlanckLikelihoodCert; and the interval form of two-sigma consistency is derived from the residual inequality. The module status is structural theorem (zero sorry, zero new RS axioms): a consistency test against the dataset attachment, not empirical confirmation of the forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.