omega_lambda
plain-language theorem explainer
Preregisters the RS dark-energy density as the named point prediction Ω_Λ = 11/16 − α/π, with no observational numbers in the file. Cosmologists auditing the C-010 chain and BIT-kernel dark-energy structure cite this closed form. The body is a record constructor fixing the prediction name and the real value from the fine-structure constant.
Claim. The preregistered point prediction for the cosmological dark-energy density parameter is $\Omega_\Lambda = \frac{11}{16} - \frac{\alpha}{\pi}$, where $\alpha$ is the electromagnetic fine-structure constant.
background
This module holds preregistered Hubble-sector predictions and deliberately contains no observational numbers. A point prediction is a named real value used downstream for verification against data, not a theorem.
The formula $\Omega_\Lambda = 11/16 - \alpha/\pi$ is the standard RS expression for the dark-energy density parameter. Upstream cosmology modules state that $11/16 = 0.6875$ is the fraction of ledger modes in the vacuum (unexcited) state over the eight-tick cycle, while $-\alpha/\pi$ is the small electromagnetic correction from matter-coupled modes. Here $\alpha$ is the fine-structure constant from the constants library ($\alpha = 1/\alpha^{-1}$).
Sibling cosmology derivations (EarlyUniverse, OmegaLambdaDerivation, CosmologicalConstantDerivation, PhaseSaturationVacuum) all instantiate the same closed form, sometimes with a locked or CODATA anchor for $\alpha$. This preregistered copy packages that value for the verification layer.
proof idea
Definition only: a noncomputable record of type PointPrediction. The name field is the string "Omega_L"; the value field is the real expression $(11:\mathbb{R})/16 - \alpha/\pi$, using the imported fine-structure constant and real $\pi$. No lemmas or tactics.
why it matters
This is the verification-layer handle for RS prediction C-010 ($\Omega_\Lambda = 11/16 - \alpha/\pi$). Downstream, CosmologicalConstantDerivation uses it to prove the weak bounds $0 < \Omega_\Lambda < 11/16$ and the tight numeric window $\Omega_\Lambda \in (0.683, 0.686)$ relied on by Planck checks and BIT-kernel modules. DarkEnergyEvolutionStructure treats positivity and the subunit bound as structural hypotheses, excluding the degenerate endpoints $\Omega_\Lambda = 0$ and $\Omega_\Lambda = 1$.
Framework link: the seed $11/16$ is the vacuum-mode fraction on the eight-tick octave (forcing-chain T7), with the $\alpha/\pi$ correction the only measured electromagnetic input. The preregistration keeps the prediction free of post-hoc observational tuning before comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.