Omega_Lambda_pos
plain-language theorem explainer
The RS dark-energy fraction Ω_Λ = 11/16 − α/π is strictly positive, so the predicted vacuum mode share is nonzero. Cosmologists and auditors of the phase-saturation vacuum module cite this as the existence half of the Ω_Λ bounds. The proof unfolds the definition and finishes by linear arithmetic from the seed inequality α/π < 11/16.
Claim. Let $\Omega_\Lambda := \frac{11}{16} - \frac{\alpha}{\pi}$. Then $0 < \Omega_\Lambda$.
background
This module identifies the cosmological dark-energy fraction with the equilibrium vacuum share of a discrete ledger under phase saturation. The explicit RS formula is $\Omega_\Lambda = 11/16 - \alpha/\pi$: a cube-geometry seed $11/16$ from passive-mode counting on $Q_3$, corrected by the electromagnetic term $\alpha/\pi$.
The seed $11/16$ is the passive-mode fraction in the eight-tick / three-dimensional ledger geometry forced upstream (T7–T8). The correction uses the in-module fine-structure constant alpha. Positivity is not automatic: it requires $\alpha/\pi < 11/16$, proved as the sibling theorem alpha_over_pi_lt_seed from $\alpha < 1/2$ and $\pi > 3$.
Local status: the algebraic definition and basic bounds are proved; the bridge from ledger saturation to cosmology remains a named hypothesis with an explicit falsifier.
proof idea
One-line term/tactic proof. Unfold $\Omega_\Lambda$ to $11/16 - \alpha/\pi$, then apply linarith with the single lemma alpha_over_pi_lt_seed ($\alpha/\pi < 11/16$). No further case splits or external analysis.
why it matters
Existence of a positive vacuum fraction is the first half of the RS answer to the cosmological-constant problem inside this module. Downstream, Omega_Lambda_bounds packages $0 < \Omega_\Lambda < 11/16$; no_vacuum_catastrophe uses the same positivity with $\Omega_\Lambda < 1$ to argue that vacuum energy is an $O(1)$ mode fraction, not a Planck-scale density needing $10^{120}$ fine-tuning; phase_saturation_vacuum_cert records omega_pos := Omega_Lambda_pos in the module certificate.
Framework landmarks: the $11/16$ seed traces to eight-tick octave and $D=3$ mode counting (T7–T8); $\alpha$ sits in the RS band near $1/137$. The algebraic positivity proved here does not close the still-open CosmicPhaseEquilibrium / vacuum_fraction_bridge hypotheses that identify ledger saturation with cosmic $\Omega_\Lambda$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.