Omega_Lambda
plain-language theorem explainer
Defines the Recognition Science dark-energy fraction as Ω_Λ = 11/16 − α/π, the cube-geometry passive-mode seed corrected by the measured fine-structure constant over π. Cosmologists and RS auditors cite it as the closed-form vacuum share of the ledger. The body is a one-line real definition; no proof obligations.
Claim. The dark-energy density parameter is the real number $\Omega_\Lambda := \frac{11}{16} - \frac{\alpha}{\pi}$, where $\alpha$ is the measured fine-structure constant (CODATA anchor).
background
This module treats dark energy as the equilibrium vacuum share of a discrete ledger with finite phase capacity. Phase-saturation pressure on that ledger appears cosmologically as vacuum energy. The geometric seed $11/16$ is the passive-mode fraction of the $Q_3$ cube mode budget; the electromagnetic correction subtracts $\alpha/\pi$.
Locally, $\alpha$ is the single measured input, bound to the CODATA external anchor (same convention as in the companion CosmologicalConstantDerivation module). The module chain is: finite ledger capacity $\to$ cosmic matter/vacuum equilibrium $\to$ vacuum fraction equals passive modes from cube geometry $\to$ $\Omega_\Lambda = 11/16 - \alpha/\pi \approx 0.6852$.
Upstream, Constants.Alpha.alpha is the symbolic fine-structure constant $1/\alpha^{-1}$; this cosmology file overrides to the numeric CODATA value so bounds and coincidence statements can be discharged numerically.
proof idea
Pure definition: unfold to the arithmetic expression $11/16 - \alpha/\pi$ on $\mathbb{R}$. No tactics, no lemmas. Downstream proofs simply unfold Omega_Lambda (or rely on simp) and finish with ring, norm_num, or linarith against positivity and upper-bound lemmas for $\alpha$.
why it matters
This is the central closed-form prediction of the PhaseSaturationVacuum module. It feeds omega_closure ($\Omega_\Lambda + \Omega_m = 1$), the structural coincidence ratio $\Omega_\Lambda/\Omega_m = O(1)$, the no-vacuum-catastrophe statement (fraction is $O(1)$, not a Planck density), and the unconditional band bounds on $\Omega_\Lambda$.
It also appears inside the hypothesis interfaces H_CosmicPhaseEquilibrium and H_ScaleInvariance: equilibrium consistency rewrites the vacuum fraction to passive_modes/mode_budget minus $\alpha/\pi$, and scale invariance asserts the same formula at every positive scale. The geometric $11/16$ seed ties to D = 3 cube combinatorics in the forcing chain; the $\alpha/\pi$ term is the sole measured EM correction. Open scaffolding remains on the bridge from ledger saturation to cosmology (vacuum_fraction_bridge) and on the cosmic-phase-equilibrium hypothesis itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.