exact_LCDM_measurement_not_RS_linear
plain-language theorem explainer
At any positive redshift, the constant ΛCDM equation of state w = −1 is unequal to the RS structural linear placeholder −1 + φ^{−44} z. Cosmologists auditing Track 4.C dark-energy discriminators cite this as the equality form of the structural split. Proof is a short contradiction: the strict inequality at z > 0 plus irreflexivity of <.
Claim. For every real redshift $z > 0$, the ΛCDM constant $w = -1$ is not equal to the structural RS placeholder $w(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: the RS deviation scale is the rung-44 factor $\varphi^{-44}$ (the same scale as baryogenesis $\eta_B = \varphi^{-44}$), not the full FPT cosmic Z-aging dynamics.
ΛCDM is encoded as the constant w_LCDM_value := -1. The structural witness is the linear placeholder w_RS_linear(z) := -1 + φ^{-44} · z, which matches ΛCDM exactly at $z = 0$ and exceeds it by the positive amount $\varphi^{-44} z$ whenever $z > 0$. The honesty note in the definition is explicit: this linear profile is a non-vacuous witness, not the claimed RS dark-energy law.
The upstream discriminator theorem states the strict inequality $w_{\mathrm{RS}}(z) > -1$ at positive redshift, proved by unfolding and positivity of $\varphi^{-44}$.
proof idea
Term-mode proof by contradiction. Assume equality of the ΛCDM constant with the linear RS placeholder at the given $z > 0$. Instantiate the upstream strict discriminator, which yields $w_{\mathrm{RS}}(z) > w_{\mathrm{ΛCDM}}$. Rewrite the left side by the assumed equality to obtain $w_{\mathrm{ΛCDM}} > w_{\mathrm{ΛCDM}}$, then discharge by irreflexivity of $<$.
why it matters
Closes the equality-form half of the Track 4.C structural discriminator: an exact ΛCDM measurement at positive redshift cannot be the RS linear witness. Together with the strict inequality sibling, it packages the claim that RS and ΛCDM split at order $\varphi^{-44}$ once $z > 0$, matching the master-plan requirement of a sub-leading, falsifiable deviation from $w = -1$.
No downstream consumers are wired yet; the natural parent is the module's master cert bundling the ΛCDM constant, the rung-44 scale, the linear witness, and the discriminator. The full functional $z$-dependence from FPT cosmic Z-aging remains open; this theorem only protects the placeholder inequality against accidental equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.