Omega_Lambda_lt_seed
plain-language theorem explainer
The RS dark-energy fraction satisfies Ω_Λ < 11/16. Cosmologists and RS auditors cite this as the strict upper bound coming from the cube-geometry seed once the positive EM correction α/π is subtracted. The proof unfolds the definition and applies linear arithmetic to positivity of α/π.
Claim. Let $\Omega_\Lambda := 11/16 - \alpha/\pi$. Then $\Omega_\Lambda < 11/16$.
background
The module derives the cosmological dark-energy fraction from phase saturation of the discrete ledger: at cosmic scale, vacuum modes equilibrate to a passive-mode fraction fixed by Q₃ geometry, giving the seed 11/16, then corrected by the measured fine-structure constant.
The RS prediction is the real number $\Omega_\Lambda = 11/16 - \alpha/\pi$ (cube-geometry seed minus the EM correction). The only upstream fact needed here is that $\alpha/\pi > 0$, which follows from positivity of $\alpha$ and of $\pi$.
proof idea
Unfold the definition $\Omega_\Lambda = 11/16 - \alpha/\pi$. Because $\alpha/\pi > 0$ (lemma alpha_over_pi_pos), subtracting a positive quantity from $11/16$ yields a strictly smaller real. linarith discharges the inequality in one step.
why it matters
This is the seed upper bound for the whole Ω_Λ package. It is the second conjunct of Omega_Lambda_bounds, the first step of the calc chains proving $\Omega_\Lambda < 1$ and the tighter numerical bound $\Omega_\Lambda < 0.69$, and a field of the certificate phase_saturation_vacuum_cert. In the module chain it sits under the proved geometric seed 11/16; the remaining open pieces are the hypotheses CosmicPhaseEquilibrium and vacuum_fraction_bridge that connect ledger saturation to cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.