omega_lambda_planck_err
plain-language theorem explainer
Fixes the Planck 2018 one-sigma uncertainty on Ω_Λ at 0.0056. Cosmology certificates cite it as the external observational scale against which the RS interval (0.683, 0.686) is compared. The body is a numeric constant definition, not a derived claim.
Claim. The Planck 2018 $1\sigma$ error on the dark-energy density fraction is $\sigma(\Omega_\Lambda)=0.0056$, so the reported measurement is $\Omega_\Lambda=0.6889\pm 0.0056$.
background
The module derives the cosmological constant fraction from eight-tick phase saturation: $\Omega_\Lambda=11/16-\alpha/\pi$, with $11/16$ the saturated Q₃-mode fraction of the 4-bit addressing budget and $\alpha/\pi$ a one-loop EM correction. The target band is $\Omega_\Lambda\in(0.680,0.700)$, tightened in certificates to $(0.683,0.686)$.
Planck 2018 reports $\Omega_\Lambda=0.6889\pm 0.0056$. This definition stores only the $1\sigma$ half-width $0.0056$ as an external anchor (parallel to the CODATA $\alpha$ input). It is not an RS-derived quantity; it is the observational ruler used when stating two-sigma consistency.
Sibling constants include the Planck central value and the RS prediction omega_lambda. Consistency is the absolute deviation bound $|\Omega_\Lambda^{\mathrm{RS}}-\Omega_\Lambda^{\mathrm{Planck}}|<2\sigma$.
proof idea
No proof. The declaration is a noncomputable real definition equal to the literal decimal $0.0056$, matching the Planck 2018 $1\sigma$ bar quoted in the module header and in the doc-comment on the consistency theorem.
why it matters
Every Planck-consistency clause in the cosmology track multiplies this error by two. The theorem rs_consistent_with_planck asserts $|\omega_\lambda-\omega_\lambda^{\mathrm{Planck2018}}|<2\cdot\omega_\lambda^{\mathrm{planck_err}}$; omegaLambdaCert packages that fact; track4A_headline and Track4ACert promote it to the Track 4.A master certificate alongside the formula $\Omega_\Lambda=11/16-\alpha/\pi$ and the $\eta_B$ rung $-44$ forced by $D=3$.
Vacuum-fluctuation structural certificates reuse the same $2\times 0.0056$ window to claim the RS closed form sits inside the Planck/DESI/SN1a band without a QFT UV cutoff. The constant therefore anchors the observational half of the dark-energy claim while the combinatorial half comes from the eight-tick octave and mode counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.