omega_lambda_bounds
plain-language theorem explainer
The declaration establishes the bounds 0 < Ω_Λ < 11/16 on the dark energy density parameter in Recognition Science units. Cosmologists working on the cosmological constant problem would cite it when linking the phi-forcing chain to observable cosmology. The proof is a term-mode construction that directly pairs the positivity lemma with the strict upper-bound lemma.
Claim. $0 < 11/16 - (α/π) ∧ 11/16 - (α/π) < 11/16$, where α denotes the fine-structure constant and Ω_Λ stands for the dark energy density parameter.
background
This theorem belongs to the RegistryPredictionsProved module, which supplies calculated proofs for items in the COMPLETE_PROBLEM_REGISTRY. It covers registry item C-010 on the cosmological constant Λ, proving both Ω_Λ > 0 and Ω_Λ < 11/16 in RS-native units. The module imports PhiForcing and Constants to access the underlying phi-ladder and alpha definitions.
proof idea
The proof is a term-mode construction that pairs the two upstream lemmas omega_lambda_positive and omega_lambda_lt_11_16 to form the required conjunction. No further tactics are invoked; the result is assembled directly from the positivity and upper-bound statements already established in the same module.
why it matters
The result supplies the core bounds for the parent theorem Omega_Lambda_bounds in CosmologicalConstantDerivation, which states THEOREM C-010.4: 0 < Ω_Λ < 11/16 ≈ 0.6875, consistent with observations (Ω_Λ ≈ 0.7). It closes the calculated proof for the geometric seed 11/16 arising from the D=3 ledger structure in the Recognition framework. The derivation connects directly to the eight-tick octave and phi-ladder without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.