omega_lambda_lt_686
plain-language theorem explainer
Upper bound Ω_Λ < 0.686 for the RS dark-energy fraction 11/16 − α/π. Cosmologists citing the RS Ω_Λ interval against Planck 2018 use this half of the sandwich. The proof unfolds the definition, inserts the exact raw value 0.6875 and the strict lower bound em_correction > 0.002, then closes by linear arithmetic.
Claim. Let $\Omega_\Lambda = 11/16 - \alpha/\pi$, where $\alpha$ is the CODATA fine-structure constant. Then $\Omega_\Lambda < 0.686$.
background
The module derives the dark-energy density parameter from phase saturation in the eight-tick ledger. The raw saturated fraction is $11/16 = 0.6875$: sixteen address slots come from $2^4$ (4-bit addressing of the 8-tick cycle), and eleven of them are the $Q_3$-symmetric vacuum modes forced by the spatial-plus-gauge sector. That raw value is recorded as omega_raw, with omega_raw_val proving equality to $0.6875$ exactly.
Electromagnetic coupling subtracts a one-loop correction $\alpha/\pi$ (the measured CODATA $\alpha$, treated as the single external anchor). The local definition is therefore $\Omega_\Lambda = \texttt{omega_raw} - \texttt{em_correction}$. Upstream, em_correction_pos2 supplies the strict inequality $\alpha/\pi > 0.002$ from $\alpha > 0.0072$ and $\pi < 3.15$. The EarlyUniverse twin definition uses the same algebraic form with the RS lock value of $\alpha$.
proof idea
Term-mode proof by unfolding and linear arithmetic. Unfold $\Omega_\Lambda$ to $\texttt{omega_raw} - \texttt{em_correction}$. Invoke omega_raw_val to replace the raw term by the literal $0.6875$. Invoke em_correction_pos2 for the strict lower bound $\texttt{em_correction} > 0.002$. Then linarith discharges $0.6875 - c < 0.686$ whenever $c > 0.002$.
why it matters
This is the upper half of the certified RS window for dark energy. Downstream, omega_lambda_interval packages it with the matching lower bound omega_lambda_gt_683 into $\Omega_\Lambda \in (0.683, 0.686)$. That interval is the hypothesis of rs_consistent_with_planck, which checks 2σ agreement with Planck 2018 ($0.6889 \pm 0.0056$).
In the broader framework the raw $11/16$ sits on the eight-tick octave (T7) and the three spatial axes (T8): the mode count $11$ is the $Q_3$ sector under the $[4,2,2]$ Gray-code asymmetry. The $\alpha/\pi$ correction is the only measured input; the combinatorial skeleton is forced. Closing both bounds converts the module claim "$\Omega_\Lambda \in (0.680, 0.700)$" into a tight, machine-checked interval usable by the preregistered Hubble prediction layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.