omega_lambda_planck2018
plain-language theorem explainer
Anchors the Planck 2018 central value Ω_Λ = 0.6889 as a real constant for numerical comparison. Cosmology certificates cite it when checking that the RS prediction 11/16 − α/π lies inside the observational band. The body is a bare numeric definition, not a derived claim.
Claim. Define the Planck 2018 central value of the dark-energy density fraction by $\Omega_\Lambda^{\mathrm{Planck2018}} := 0.6889$.
background
The module derives the cosmological constant fraction from phase saturation on the eight-tick cycle. The combinatorial raw fraction is $11/16$ (Q₃-symmetric modes over the $2^4$ tick-addressing budget), corrected by a one-loop EM term $\alpha/\pi$, yielding $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.685$ in a narrow interval about $(0.683, 0.686)$.
Observational comparison needs a fixed external anchor. Planck 2018 reports $\Omega_\Lambda = 0.6889 \pm 0.0056$ (1σ). This definition stores only the central value; the companion error bar is a separate constant used in the 2σ consistency theorems.
In RS units the prediction is structural (eight-tick octave, $D=3$ mode counting) plus one measured input $\alpha$. The Planck number is not derived inside the framework; it is the external datum against which the interval is checked.
proof idea
No proof. The declaration is a noncomputable real definition equal to the literal decimal $0.6889$. Downstream theorems unfold it and discharge numeric goals with norm_num and absolute-value bounds.
why it matters
Supplies the observational center used by rs_consistent_with_planck, which asserts $|\Omega_\Lambda - 0.6889| < 2\times 0.0056$, and by the certificate omegaLambdaCert. Track 4.A headline and Track4ACert fold the same comparison into the joint claim that $\Omega_\Lambda = 11/16 - \alpha/\pi$ overlaps Planck within 2σ while the baryon rung $-44$ is forced by $D=3$.
Vacuum-fluctuation structural theorems reuse the constant (sometimes inlined as $0.6889$) to state cutoff-independent agreement with the Planck/DESI/SN1a band. Gravity's master theorem and the verification likelihood module also pin their Planck-central references here, so a single numeric source feeds every cosmology consistency edge.
Framework landmarks: eight-tick octave and $D=3$ force the $11/16$ combinatorics; $\alpha$ is the sole external coupling. This def does not touch T5–T8 forcing; it only closes the observational side of Track 4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.