omega_lambda_positive
plain-language theorem explainer
Researchers resolving the cosmological constant smallness problem cite the inequality establishing positive Ω_Λ from the derived fine-structure constant. The result confirms 11/16 - α/π > 0 using the structural bound alphaInv > 2. The tactic sequence unfolds definitions, applies positivity and field simplification, then uses linarith on the chained inequalities.
Claim. $11/16 - (α/π) > 0$, where α denotes the fine-structure constant obtained as 1/α_inv with α_inv constructed from the geometric seed 4π·11 and gap correction, and the bound α_inv > 2 holds by the exponential inequality.
background
The RegistryPredictionsProved module supplies calculated proofs for predictions in the COMPLETE_PROBLEM_REGISTRY, specifically item C-010 on the cosmological constant. Alpha denotes the fine-structure constant defined as 1 over alphaInv, with alphaInv constructed as alpha_seed times exp of minus f_gap over alpha_seed, and alpha_seed equal to 4 pi times 11. The key upstream result alphaInv_gt_2 establishes alphaInv > 2 via the inequality exp(-t) ≥ 1 - t and numerical comparison of the seed minus gap exceeding 2.
proof idea
The tactic proof begins by proving positivity of alphaInv and alpha through unfolding and the positivity tactic. It derives alpha < 1/2 by rewriting alpha as 1/alphaInv and applying div_lt_div_iff with linarith on alphaInv_gt_2. It then invokes Real.pi_gt_three to obtain pi > 1, shows alpha/pi < alpha by div_lt_self, and finishes with linarith to reach the target inequality.
why it matters
This theorem supplies the positivity half of the bounds in omega_lambda_bounds and directly defines Omega_Lambda_positive in the CosmologicalConstantDerivation module. It addresses the C-010 registry item for Ω_Λ > 0 and contributes to the existence of the RegistryPredictionsCert. The argument rests on the alpha derivation from the structural seed in the phi-forcing framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.