w_LCDM_value_eq_neg_one
plain-language theorem explainer
The ΛCDM dark-energy equation of state is exactly the constant −1, independent of redshift. Cosmologists comparing RS Track 4.C predictions against ΛCDM cite this as the baseline anchor. The proof is pure definitional reflexivity: the constant is defined as −1.
Claim. The ΛCDM dark-energy equation-of-state constant equals $-1$: $w_{\Lambda\mathrm{CDM}} = -1$.
background
Track 4.C of the RS quantum-gravity master plan asks for a falsifiable dark-energy equation of state $w(z)$ that differs at sub-leading order from ΛCDM. In standard cosmology, a pure cosmological constant has constant equation of state $w = -1$ at every redshift; that is the baseline against which any RS deviation is measured.
This module packages that baseline as the real constant w_LCDM_value, defined to be $-1$. The RS side introduces the rung-44 forcing scale $\varphi^{-44}$ (the same scale that appears in baryogenesis via $\eta_B = \varphi^{-44}$), and a structural linear placeholder $w_{\mathrm{RS}}(z) = -1 + \varphi^{-44}\cdot z$. Discriminator theorems then compare the two at $z=0$ and at positive redshift.
The present declaration simply records that the ΛCDM constant really is $-1$, so downstream statements can quote a named equality rather than unfold a definition ad hoc.
proof idea
One-line term proof by rfl. The definition of the ΛCDM equation-of-state constant is literally the real number $-1$, so equality holds by definitional reduction with no lemmas required.
why it matters
This equality is the first conjunct of the Track 4.C one-statement theorem, which asserts that ΛCDM has $w=-1$, that $\varphi^{-44}>0$, that the RS linear placeholder matches $-1$ at $z=0$, and that it strictly exceeds $-1$ at positive $z$ by exactly $\varphi^{-44}\cdot z$. It is also the w_LCDM_constant field of the master certificate darkEnergyWofZStructuralCert.
Without a named proof that the baseline is $-1$, the discriminator inequalities would have to re-unfold the definition at every use site. The result sits at the ΛCDM end of the structural comparison; the RS end is forced by the same rung-44 scale that appears in the phi-ladder baryogenesis story. The specific FPT cosmic Z-aging $z$-dependence remains future work; this module only ships the algebraic discriminator skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.