planck_sigma
plain-language theorem explainer
Numeric constant fixing the Planck 2018 one-sigma width at 0.0056. Cosmologists citing the BIT Ω_Λ gap retirement use it as the observational yardstick against which the maximum-amplitude corrected density is compared. The body is a bare real literal; no proof content.
Claim. The Planck 2018 one-sigma uncertainty is the real number $0.0056$.
background
The module forces the dark-energy deviation kernel $K(z)$ from two premises: rung factorization (attenuation multiplies across independent $\varphi$-rungs) and single-rung balance (one rung attenuates by the unique positive fixed point $\varphi^{-1}$ of $\rho=1/(1+\rho)$). The forced law is $\mathrm{occ},n=\varphi^{-n}$, equivalently $1/(1+z)$ on the lattice $1+z=\varphi^n$, which pins the scale-free power $s=1$ and yields a CPL form on the thawing line with $w(z)\ge -1$ always.
Against that forced shape the module compares a bare RS $\Omega_\Lambda$ to a maximum-amplitude BIT-corrected value. The comparison needs an external observational width: the Planck 2018 $1\sigma$ band. This definition supplies that width as a fixed real constant. Upstream kernel families (constant, $1/(1+z)$, exponential) and the cost/functional-equation infrastructure fix the shape side; the constant itself is pure observational input.
proof idea
Definition by numeric literal. No tactics, no lemmas, no reduction: the real $0.0056$ is assigned directly as the Planck 2018 one-sigma value used downstream.
why it matters
Feeds the retirement certificate omega_gap_explanation_retired, which asserts three conjuncts: the max-amplitude corrected $\Omega_\Lambda$ lies below the bare RS value; its distance from the Planck central value exceeds this one-sigma width in the adverse direction; and the forced kernel keeps $w(z)\ge -1$ at every physical redshift, so neither shape nor amplitude can flip the sign. Together those kill the hypothesis that BIT cosmic aging closes the Planck–RS $\Omega_\Lambda$ gap.
In the broader Recognition chain this sits after T5–T6 (unique $J$ and $\varphi$) and the rung-dilution forcing that selects $K(z)=(1+z)^{-1}$. The open item remains the today-amplitude $\delta w_0\in(0,J(\varphi)]$; the constant here only calibrates the observational side of the gap test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.