wLambda
plain-language theorem explainer
wLambda fixes the dark energy equation of state at the cosmological constant value -1 as the Recognition Science baseline before BIT perturbations. Cosmologists using the RS framework cite this constant when establishing the zero-order EoS and deriving the interval (-1 - J(φ), -1) for w_0. The declaration is introduced by direct assignment with no computation or lemma calls.
Claim. The baseline dark energy equation-of-state parameter is defined by $w_0 = -1$.
background
The module examines the dark energy equation of state in S3 cosmology depth, starting from the cosmological constant case. The module documentation states that the BIT correction deviates from w = -1 with the RS prediction w_0 ∈ (-1 - J(φ), -1) ≈ (-1.13, -1), and that |w_0 + 1| ≤ J(φ) ≈ 0.118 follows from the OmegaLambdaBITKernelBand. The upstream correction definition supplies the φ-ladder finite-N factor 1/(φ N) used for channel capacity adjustments in the same framework.
proof idea
The declaration is a direct definition that assigns the real number -1 with no lemma applications or tactics.
why it matters
This baseline enters the DarkEnergyEoSCert structure, which requires baseline_w : wLambda = -1 together with the count of five dark energy models. It anchors the RS prediction for the dark energy EoS band derived from the J(φ) correction and supports the claim |w_0 + 1| ≤ J(φ) in the cosmology depth section. The definition closes the zero-order step before the forcing-chain landmarks T5-T8 are applied to the perturbed EoS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.