omega_lambda_planck_likelihood_one_statement
plain-language theorem explainer
RS dark-energy density Ω_Λ sits inside the Planck 2018 two-sigma band, the residual is strictly below two sigma, the falsifier-register attachment is currently sensitive, and the master likelihood certificate is inhabited. Cosmologists auditing the §7 Ω_Λ row cite this as the single conjunction closing the dataset-specific likelihood attachment. Proof is a four-field term packing residual, interval, sensitivity, and certificate-inhabitance lemmas.
Claim. The residual between the RS prediction $\Omega_\Lambda$ and the Planck 2018 central value is strictly less than twice the Planck uncertainty; equivalently $\Omega_\Lambda$ lies in the open two-sigma interval about that central value; the Planck $\Omega_\Lambda$ dataset attachment is currently sensitive; and the master Planck-likelihood certificate is inhabited.
background
Recognition Science predicts the dark-energy density parameter as $\Omega_\Lambda = 11/16 - \alpha/\pi$, where $11/16$ is the vacuum-mode fraction on the eight-tick ledger cycle and $-\alpha/\pi$ is the electromagnetic correction from matter-coupled modes. The derived numerical band is $0.683 < \Omega_\Lambda < 0.686$.
This module upgrades the falsifier-register cosmological-constant row to a dataset-specific likelihood-style certificate against Planck 2018 TT,TE,EE+lowE+lensing, which reports $\Omega_\Lambda = 0.6889 \pm 0.0056$. The attachment records positive sensitivity and a target scale equal to the width of the RS band. The test is framed as two-sigma consistency, not empirical confirmation. Zero sorry and zero new RS-specific axioms.
proof idea
Term-mode proof that builds a four-fold conjunction from four prior results in order: the residual bound (residual strictly below two Planck sigma), the equivalent open-interval form of that bound (obtained from the residual via the absolute-value characterization of open intervals), reflexivity for the currently-sensitive flag on the dataset attachment, and inhabitance of the master certificate structure (which packages sigma positivity, residual, interval, and dataset activity).
why it matters
Closes the structural upgrade of the §7 Ω_Λ falsifier-register row from a bare dataset attachment to a likelihood-style Lean certificate. Packages residual, interval, sensitivity, and certificate inhabitance into one citation point for the verification layer. Downstream use is currently empty, so this is a leaf certificate in the verification graph. Ties the eight-tick vacuum fraction $11/16$ and the RS fine-structure correction into a concrete cosmological consistency check against Planck 2018, without claiming empirical confirmation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.