omega_lambda_pos
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.