w_RS_linear_eq_LCDM_at_zero
plain-language theorem explainer
At redshift zero the structural RS placeholder for the dark-energy equation of state equals the ΛCDM constant −1. Cosmologists comparing RS Track 4.C to ΛCDM cite this as the shared present-day anchor. The proof is a one-line term that reuses the evaluation of the linear profile at z = 0.
Claim. The structural RS dark-energy profile satisfies $w_{\mathrm{RS}}^{\mathrm{lin}}(0) = w_{\Lambda\mathrm{CDM}}$, where $w_{\Lambda\mathrm{CDM}} = -1$ and $w_{\mathrm{RS}}^{\mathrm{lin}}(z) = -1 + \varphi^{-44}\, z$.
background
Track 4.C of the quantum-gravity master plan asks for a falsifiable RS equation of state $w(z)$ that matches ΛCDM today but deviates at sub-leading order. This module supplies the algebraic discriminator, not the full FPT Z-aging dynamics: a linear placeholder $w_{\mathrm{RS}}^{\mathrm{lin}}(z) := -1 + \varphi^{-44}, z$.
Here $w_{\Lambda\mathrm{CDM}}$ is the constant $-1$. The scale $\varphi^{-44}$ is the same rung-44 factor that appears in baryogenesis ($\eta_B = \varphi^{-44}$). The companion lemma already shows $w_{\mathrm{RS}}^{\mathrm{lin}}(0) = -1$ by unfolding and ring arithmetic; the present statement only renames that value as the ΛCDM constant.
proof idea
One-line term proof: apply w_RS_linear_at_zero, which unfolds $w_{\mathrm{RS}}^{\mathrm{lin}}(0) = -1 + \varphi^{-44}\cdot 0$ and reduces by ring to $-1$. Definitional equality of $w_{\Lambda\mathrm{CDM}}$ with $-1$ finishes the identification.
why it matters
This is the present-day matching condition for the Track 4.C structural discriminator. Downstream siblings use it to isolate the positive-redshift gap: at $z > 0$ the RS linear profile exceeds $-1$ by exactly $\varphi^{-44}, z$, giving a concrete, rung-44-suppressed departure from ΛCDM. The module status is structural theorem (zero sorry); the honest caveat remains that the linear slope is a non-vacuous witness, not the final RS $w(z)$ from FPT cosmic Z-aging. That functional form is left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.