Omega_Lambda_bounds
plain-language theorem explainer
The RS dark-energy fraction Ω_Λ = 11/16 − α/π is strictly positive and strictly below the cube-geometry seed 11/16. Anyone citing the phase-saturation vacuum prediction uses this as the basic consistency window against Ω_Λ ≈ 0.7. The proof is a one-line pairing of the positivity and seed-upper-bound lemmas already proved in-module.
Claim. Let $\Omega_\Lambda := 11/16 - \alpha/\pi$, with $\alpha$ the measured fine-structure constant. Then $0 < \Omega_\Lambda < 11/16$.
background
This module identifies the cosmological dark-energy fraction with the equilibrium vacuum share of a phase-saturated discrete ledger. The explicit RS formula is $\Omega_\Lambda = 11/16 - \alpha/\pi$: the geometric seed $11/16$ comes from passive-mode counting on the $Q_3$ cube, and the correction subtracts the electromagnetic share $\alpha/\pi$ using the single measured input $\alpha$ (CODATA anchor).
The seed $11/16 = 0.6875$ already sits near the observed $\Omega_\Lambda \approx 0.7$; subtracting a positive $\alpha/\pi$ pulls the prediction slightly below the seed. Upstream, positivity of $\alpha/\pi$ and the elementary comparison $\alpha < 1/2$ (with $\pi > 3$) supply the arithmetic needed for both sides of the bound. The companion derivation module records the same statement as theorem C-010.4.
proof idea
Term-mode proof: the conjunction constructor pairs two already-proved facts. Left conjunct is Omega_Lambda_pos (strict positivity of $11/16 - \alpha/\pi$). Right conjunct is Omega_Lambda_lt_seed, which unfolds the definition and applies linarith to positivity of $\alpha/\pi$, yielding the strict inequality against the bare seed $11/16$. No new arithmetic is introduced here.
why it matters
This is the basic bound surface for the phase-saturation vacuum prediction. Downstream it is re-exported as C-010.4 in CosmologicalConstantDerivation.Omega_Lambda_bounds and is consumed by the forcing-chain bridge t6_t8_to_cosmology_constants_bridge_holds, which routes T6 ($\varphi$ uniqueness) and T8 ($D = 3$) into theorem-backed cosmology constants while keeping empirical bands separate from exact identities.
Within the module status list it closes the "definition and basic bounds" item for $\Omega_\Lambda$. It does not discharge the still-open hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge that connect ledger saturation to cosmology; those remain explicit hypothesis interfaces with falsifiers. The geometric seed $11/16$ itself is the combinatorial output of the proved mode-budget / passive-mode counting on $Q_3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.