rs_consistent_with_planck
plain-language theorem explainer
The RS dark-energy fraction Ω_Λ lies inside the Planck 2018 two-sigma band: |Ω_Λ − 0.6889| < 2 × 0.0056. Cosmologists and RS auditors cite it as the observational consistency check for the combinatorial formula Ω_Λ = 11/16 − α/π. The proof reduces the absolute-value claim to the already-proved open interval (0.683, 0.686) and finishes by linear arithmetic.
Claim. Let $\Omega_\Lambda = 11/16 - \alpha/\pi$ be the RS dark-energy fraction, and let the Planck 2018 central value and $1\sigma$ error be $0.6889$ and $0.0056$. Then $|\Omega_\Lambda - 0.6889| < 2 \cdot 0.0056$.
background
This module derives the cosmological constant fraction from phase saturation on the eight-tick ledger. The raw saturated fraction is the combinatorial ratio $11/16$: sixteen is the $2^4$ addressing of the eight-tick cycle, and eleven is the $Q_3$-symmetric mode count forced by the $[4,2,2]$ Gray-code asymmetry (four dominant-axis flips plus four second-axis activations plus two plus one). An electromagnetic one-loop correction $\alpha/\pi$ is then subtracted, giving the closed form $\Omega_\Lambda = 11/16 - \alpha/\pi$.
Upstream, omega_lambda is defined as that difference (equivalently omega_raw - em_correction with omega_raw = 0.6875). The sibling bounds omega_lambda_gt_683 and omega_lambda_lt_686 already place the prediction in the open interval $(0.683, 0.686)$. Planck 2018 is recorded as the constants $0.6889 \pm 0.0056$. The module uses one measured input (CODATA $\alpha$); the integer combinatorics are structural.
proof idea
Unfold the Planck central value and error bar to the literals $0.6889$ and $0.0056$. Compute $2 \times 0.0056 = 0.0112$ by norm_num, rewrite the goal as an absolute-value inequality, and split it into the two-sided form $-0.0112 < \Omega_\Lambda - 0.6889 < 0.0112$. The left half follows from the lower bound $\Omega_\Lambda > 0.683$ by linarith; the right half follows from the upper bound $\Omega_\Lambda < 0.686$ by linarith. No new analytic content is introduced beyond those two interval lemmas.
why it matters
This is the observational gate for the entire $\Omega_\Lambda$ derivation. It is packaged into omegaLambdaCert as the planck_consistent field, and it appears verbatim in the Track 4.A headline theorem, which simultaneously pins $\Omega_\Lambda \in (0.683, 0.686)$ and the baryon-to-photon rung $-44$ from $D = 3$ plus one measured $\alpha$. The vacuum-fluctuation structural certificate and its one-statement form reuse the same residual bound to assert cutoff-independence of the combinatorial formula. Downstream verification (omegaLambda_residual_lt_two_sigma) is a one-line re-export. In the forcing chain this sits after T7 (eight-tick octave) and T8 ($D = 3$), which supply the mode budget that produces the integer $11$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.