planckOmegaLambdaTwoSigma_pos
plain-language theorem explainer
The two-sigma Planck 2018 tolerance on ΩΛ is strictly positive. Anyone assembling the ΩΛ likelihood-style certificate cites this as a structural positivity lemma. The proof unfolds the tolerance as twice the one-sigma error and multiplies two positive reals.
Claim. The two-sigma Planck tolerance $2\sigma_{\Omega_\Lambda}^{\mathrm{Planck}}$ is strictly positive: $0 < 2\sigma_{\Omega_\Lambda}^{\mathrm{Planck}}$.
background
This module attaches a likelihood-style Lean certificate to the RS dark-energy density prediction against Planck 2018 TT,TE,EE+lowE+lensing. The RS side comes from Cosmology.OmegaLambdaDerivation: $\omega_\Lambda = 11/16 - \alpha/\pi$, forced into the open interval $(0.683, 0.686)$. The dataset side records $\Omega_\Lambda = 0.6889 \pm 0.0056$.
The one-sigma error is the positive real planckOmegaLambdaSigma (equal to the Planck error $0.0056$). The two-sigma tolerance is defined by planckOmegaLambdaTwoSigma := 2 * planckOmegaLambdaSigma. Upstream, planckOmegaLambdaSigma_pos already shows $0 < \sigma$ by unfolding and norm_num. The present lemma lifts that to the doubled band used in residual comparisons.
proof idea
One-line term proof after unfold. Expand planckOmegaLambdaTwoSigma to $2\cdot\sigma$. Apply real multiplication-positivity (mul_pos) to the pair $0 < 2$ (discharged by norm_num) and $0 < \sigma$ (the sibling lemma planckOmegaLambdaSigma_pos). No case splits or inequalities beyond positivity of a product of positives.
why it matters
Feeds the certificate record omegaLambdaPlanckLikelihoodCert as the field two_sigma_pos. That certificate packages five facts: both $\sigma$ and $2\sigma$ positive, residual strictly below two sigma, interval form of the same bound, and the dataset attachment flagged active. Without positivity of the tolerance, the residual comparison $|\omega_\Lambda - 0.6889| < 2\sigma$ is ill-typed as a strict band test.
In the broader RS verification layer this upgrades the §7 falsifier-register ΩΛ row from a bare dataset pointer to a closed, zero-sorry consistency certificate. It is explicitly a consistency test, not empirical confirmation. The numerical content sits downstream of the forcing chain only indirectly (via the $\alpha$-dependent formula for $\omega_\Lambda$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.