omega_lambda_lt_11_16
plain-language theorem explainer
The inequality shows that the Recognition Science dark energy density satisfies Ω_Λ < 11/16. Cosmologists deriving upper bounds on the cosmological constant from the fine-structure constant would cite this when closing registry item C-010. The argument reduces to positivity of α/π followed by a direct linear inequality after unfolding the exponential definition of alphaInv.
Claim. $11/16 - (α/π) < 11/16$, where α is the fine-structure constant given by the resummation α = 1/(α_seed ⋅ exp(−f_gap/α_seed)) with geometric seed α_seed = 4π ⋅ 11.
background
The Registry Predictions module supplies calculated proofs for COMPLETE_PROBLEM_REGISTRY items, including C-010 on the cosmological constant with the explicit bound Ω_Λ < 11/16. The constant α is defined via alphaInv = alpha_seed ⋅ exp(−(f_gap/alpha_seed)) where alpha_seed = 4 ⋅ π ⋅ 11 and f_gap is the gap weight from DFT-8 projection. Upstream lemmas establish positivity of alphaInv by unfolding to the seed and applying exp positivity, together with Real.pi_pos.
proof idea
The proof first constructs a hypothesis that α/π > 0 by unfolding alpha to 1/alphaInv, applying positivity to alphaInv > 0 (via alpha_seed and exp) and to π, then concludes the target inequality by linarith. It is a direct algebraic reduction that relies on the positivity infrastructure imported from Mathlib.
why it matters
This declaration supplies the upper bound for THEOREM C-010.2 (Omega_Lambda_lt_upper_bound) and is conjoined into omega_lambda_bounds and the registry_predictions_cert_exists certificate. It closes the calculated prediction for the cosmological constant using the alpha band (137.03–137.039) and the structural seed from the phi-ladder, while the remaining numerical gap bound f_gap < alpha_seed − 2 stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.