Omega_Lambda_lt_one
plain-language theorem explainer
The RS dark energy fraction Ω_Λ is strictly less than one (subunitary). Cosmologists working the phase-saturation vacuum model cite this to close the density budget and to discharge the no-vacuum-catastrophe certificate. Proof is a two-line calc: the seed bound Ω_Λ < 11/16, then 11/16 < 1 by norm_num.
Claim. The Recognition Science dark energy fraction $\Omega_\Lambda = \frac{11}{16} - \frac{\alpha}{\pi}$ satisfies $\Omega_\Lambda < 1$.
background
This module treats dark energy as the equilibrium vacuum share of a discrete ledger under phase saturation. The geometric seed 11/16 is the passive-mode fraction from Q₃ cube counting; subtracting the electromagnetic correction α/π yields the RS prediction Ω_Λ ≈ 0.685.
Ω_Λ is defined by that formula. The sibling theorem already gives Ω_Λ < 11/16 because α/π > 0. The present result lifts the seed bound to the subunitary statement required for a closed cosmic density budget (Ω_Λ + Ω_m = 1 with both positive).
proof idea
Two-step calc proof. First apply the upstream seed inequality Ω_Λ < 11/16. Then discharge the pure numerical comparison 11/16 < 1 by norm_num. No unfolding of the definition of Ω_Λ is needed at this layer; positivity of α/π was already consumed upstream.
why it matters
Three downstream consumers. The coincidence-ratio theorem uses the bound (with density closure) to force Ω_m < 1/2 and hence Ω_Λ/Ω_m > 1, so the coincidence ratio is O(1) by construction. The no-vacuum-catastrophe theorem packages Ω_Λ < 1 ∧ Ω_Λ > 0 to argue that vacuum energy is an O(1) mode fraction, not a Planck-scale density, dissolving the 10^120 discrepancy. The phase-saturation vacuum certificate records the subunitary bound as the field omega_lt_one. In the module chain this is the upper half of the geometric vacuum bound, complementary to positivity; the deeper CosmicPhaseEquilibrium and vacuum_fraction_bridge links remain hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.