Pith. sign in
module module moderate

IndisputableMonolith.Verification.OmegaLambdaPlanckLikelihood

show as:
view Lean formalization →

Verification module that pins the RS-derived dark-energy fraction against the Planck 2018 Ω_Λ measurement. It records the Planck central value and uncertainty, forms the residual to the derived Ω_Λ, and proves that residual lies inside the two-sigma band. Cosmologists checking the Ω_Λ falsifier row cite the certificate and the interval lemma. The argument is arithmetic comparison of fixed rationals plus positivity of the reported sigma.

claimLet $\Omega_\Lambda^{\mathrm{RS}} = 11/16 - \alpha/\pi$ be the derived dark-energy fraction and let $\Omega_\Lambda^{\mathrm{P18}}$, $\sigma_{\Lambda}$ be the Planck 2018 central value and $1\sigma$ error. The module asserts $|\Omega_\Lambda^{\mathrm{RS}} - \Omega_\Lambda^{\mathrm{P18}}| < 2\sigma_{\Lambda}$, packages this as a likelihood certificate, and marks the corresponding falsifier-register dataset attachment as active.

background

Recognition Science derives the cosmological constant fraction from phase saturation as $\Omega_\Lambda = 11/16 - \alpha/\pi$, and the upstream derivation module already proves the closed interval claim $\Omega_\Lambda \in (0.680, 0.700)$. That band is the theoretical prediction fed into observational checks.

This verification module sits in the falsifier-register stack. Upstream FalsifierRegisterDatasets attaches named datasets and sensitivity records to every row of the quantum-gravity master plan §7 register. Here the attached observable is Planck 2018 $\Omega_\Lambda$: a fixed central value, a positive $1\sigma$ width, and the two-sigma threshold built from them.

Sibling definitions introduce the residual $\Omega_\Lambda^{\mathrm{RS}} - \Omega_\Lambda^{\mathrm{P18}}$, positivity lemmas for the reported errors, and a certificate type that packages the two-sigma containment for the likelihood layer.

proof idea

The module is mostly concrete numerical scaffolding plus short comparison proofs. Central value and sigma are definitional constants. Residual is their difference against the derived $\Omega_\Lambda$. Positivity of $\sigma$ and $2\sigma$ is immediate from the positive literal. The main lemmas reduce to checking that the absolute residual is strictly less than twice the Planck sigma, then rephrasing that inequality as membership in the closed two-sigma interval around the Planck central value. A certificate record and an inhabited instance expose the result to the register; a boolean/Prop flag marks the dataset attachment active.

why it matters in Recognition Science

The parent consumer is FalsifierLikelihoodRegister, which aggregates Sessions 107--115 into the dataset-specific likelihood and status layer over the §7 falsifier register. Without this module, the $\Omega_\Lambda$ row would lack a Planck-anchored residual bound and an active attachment flag.

It closes the observational half of the upstream core claim that $\Omega_\Lambda = 11/16 - \alpha/\pi$ lands in $(0.680, 0.700)$: the derivation supplies the RS number; this file shows that number is compatible with Planck 2018 at two sigma. In the broader RS chain this is a late verification step, not a forcing-chain (T0--T8) lemma, but it is required for the falsifier register to report a live, data-backed status on dark energy.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)