w_RS_linear_distinct_from_LCDM_abs
plain-language theorem explainer
At any positive redshift z, the absolute gap between the structural RS linear w(z) placeholder and the ΛCDM constant w = −1 is strictly positive. Cosmologists citing Track 4.C use this absolute-value form of the discriminator. The proof lifts the signed strict inequality via positivity of the difference and abs_of_pos.
Claim. For every real redshift $z > 0$, $\lvert w_{\mathrm{RS,lin}}(z) - w_{\Lambda\mathrm{CDM}}\rvert > 0$, where $w_{\Lambda\mathrm{CDM}} = -1$ and $w_{\mathrm{RS,lin}}(z) = -1 + \varphi^{-44}\, z$.
background
Track 4.C of the quantum-gravity master plan asks for a falsifiable dark-energy equation of state that differs at sub-leading order from ΛCDM's strict $w = -1$. This module ships the algebraic discriminator only: a structural linear-in-$z$ placeholder, not the full FPT cosmic Z-aging dynamics.
ΛCDM is encoded as the constant $w_{\Lambda\mathrm{CDM}} = -1$. The RS witness is $w_{\mathrm{RS,lin}}(z) := -1 + \varphi^{-44}, z$, with $\varphi^{-44}$ the rung-44 forcing scale (same order as baryogenesis $\eta_B = \varphi^{-44}$). At $z = 0$ the two agree; at $z > 0$ the deviation is exactly $\varphi^{-44}, z > 0$.
The signed discriminator already proves $w_{\mathrm{RS,lin}}(z) > w_{\Lambda\mathrm{CDM}}$ for $z > 0$. The present statement rewrites that gap in absolute value, matching the usual observational language of $|w + 1|$.
proof idea
Apply the signed discriminator w_RS_linear_distinct_from_LCDM_at_positive_z to obtain $w_{\mathrm{RS,lin}}(z) > w_{\Lambda\mathrm{CDM}}$. Rewrite as $0 < w_{\mathrm{RS,lin}}(z) - w_{\Lambda\mathrm{CDM}}$ by linarith. Because the difference is positive, abs_of_pos replaces the absolute value by the difference itself, and the same positivity witness finishes the goal.
why it matters
Closes the absolute-value packaging of the Track 4.C structural discriminator in DarkEnergyWofZStructural. The module status is structural theorem (0 sorry): RS predicts a sub-leading $w(z)$ deviation suppressed by $\varphi^{-44}$, distinct from ΛCDM's $w \equiv -1$. The linear placeholder $w = -1 + \varphi^{-44}, z$ is an honest non-vacuous witness; the true FPT Z-aging $z$-dependence remains future work. No downstream consumers yet; sibling lemmas record the exact deviation magnitude $\varphi^{-44}, z$ and a falsifier threshold. Ties to the φ-ladder cosmology track via the shared rung-44 scale with baryogenesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.