omega_lambda_pos
Omega_lambda_pos establishes that the RS dark energy density parameter exceeds zero. Cosmologists citing the ledger-mode derivation of the dark sector use it to confirm dark energy exists from the eight-tick vacuum fraction. The tactic proof unfolds the definition, pulls in bounds on alphaLock and pi, reduces the correction term below 11/16 via nlinarith, and closes with linarith.
claim$0 < 11/16 - alphaLock / pi$, where $alphaLock = (1 - phi^{-1})/2$ is the locked fine-structure constant.
background
The EarlyUniverse module derives initial conditions and dark-sector parameters from the Recognition framework. omega_lambda is defined as 11/16 minus alphaLock over pi; the constant 11/16 counts the fraction of unexcited ledger modes inside the eight-tick cycle, while the alphaLock/pi term subtracts the small matter-coupled perturbation. alphaLock itself equals (1 - 1/phi)/2, with phi the self-similar fixed point forced by the UnifiedForcingChain.
proof idea
Unfold omega_lambda to reach 11/16 - alphaLock / pi > 0. Instantiate alphaLock_lt_one, alphaLock_pos, Real.pi_pos and Real.pi_gt_three. Establish the auxiliary alphaLock / pi < 11/16 by rewriting with div_lt_div_iff0 and applying nlinarith to the supplied bounds. linarith then discharges the goal.
why it matters in Recognition Science
Supplies the positivity half of the conjunction proved in cosmological_constant_resolution, which resolves D-003 by equating the cosmological constant to the vacuum-mode fraction rather than renormalized QFT energy. It is also used in perpetual_complexity to guarantee ongoing complexity generation under expansion and coprimality. The result realizes the eight-tick octave (T7) contribution to the dark sector and places the numerical prediction inside the observed alpha band.
scope and limits
- Does not compute a numerical value for omega_lambda beyond the sign.
- Does not incorporate supernova or CMB data.
- Does not derive the Friedmann equations or scale-factor evolution.
- Does not address alternative dark-energy mechanisms outside the ledger model.
Lean usage
theorem cosmological_constant_bounds : 0 < omega_lambda ∧ omega_lambda < 1 := cosmological_constant_resolutionformal statement (Lean)
46theorem omega_lambda_pos : 0 < omega_lambda := by
proof body
Tactic-mode proof.
47 unfold omega_lambda
48 have h_alpha := alphaLock_lt_one
49 have h_alpha_pos := alphaLock_pos
50 have h_pi := Real.pi_pos
51 have h_pi_gt3 := Real.pi_gt_three
52 have h1 : alphaLock / Real.pi < 11 / 16 := by
53 rw [div_lt_div_iff₀ Real.pi_pos (by norm_num)]
54 nlinarith [alphaLock_lt_one, Real.pi_gt_three]
55 linarith
56
57/-- Ω_Λ < 1 (subunitary). -/