darkEnergyWofZStructuralCert
plain-language theorem explainer
Packages the Track 4.C structural dark-energy equation-of-state certificate: ΛCDM has constant w = −1, the RS linear placeholder is −1 + φ^{−44} z, they agree at z = 0 and separate by exactly φ^{−44} z for z > 0, with positive falsifier thresholds and named redshift bands. Cosmologists citing the RS Ω_Λ / w(z) discriminator use this bundle. The body is a pure structure inhabitant wiring eight already-proved lemmas.
Claim. There exists a master certificate recording: the ΛCDM dark-energy equation of state equals $-1$; the rung-44 scale $\varphi^{-44}$ is positive; the RS linear placeholder $w_{\mathrm{RS}}(z) = -1 + \varphi^{-44} z$ equals the ΛCDM value at $z = 0$ and strictly exceeds it for every $z > 0$; the deviation equals $\varphi^{-44} z$; the falsifier threshold is positive at every positive redshift; the named bands at $z = 1/2$ and $z = 1$ hold; any measurement closer to ΛCDM than the threshold cannot equal the RS prediction; and the honest-scope placeholder is definitional.
background
Track 4.C of the quantum-gravity master plan asks for a falsifiable RS dark-energy equation of state $w(z)$ that differs at sub-leading order from ΛCDM's strict $w = -1$, via the $\varphi$-rung dynamical history (FPT cosmic Z-aging). This module closes only the algebraic discriminator, not the full dynamical $z$-dependence.
ΛCDM is encoded as the constant $w_{\mathrm{LCDM}} = -1$. The RS scale is $\varphi^{-44}$ (the same rung that appears in baryogenesis $\eta_B = \varphi^{-44}$). The structural RS witness is the linear placeholder $w_{\mathrm{RS}}(z) := -1 + \varphi^{-44}, z$. The falsifier threshold at redshift $z$ is the absolute separation $|w_{\mathrm{RS}}(z) - w_{\mathrm{LCDM}}| = \varphi^{-44} z$.
The structure DarkEnergyWofZStructuralCert bundles constancy of ΛCDM, positivity of $\varphi^{-44}$, matching at $z = 0$, strict separation for $z > 0$, exact deviation magnitude, positive thresholds, named bands at $z = 1/2$ and $z = 1$, a measurement-separation falsifier, and an honest-scope placeholder.
proof idea
Pure structure construction: each field is filled by an existing lemma. Constancy of ΛCDM is w_LCDM_value_eq_neg_one (definitional rfl). Positivity of $\varphi^{-44}$ is phi_neg_44_pos (positive base under integer power). Matching at zero and the strict inequality for $z > 0$ are w_RS_linear_at_zero and w_RS_linear_distinct_from_LCDM_at_positive_z. Deviation magnitude is w_RS_linear_deviation_magnitude. Threshold positivity is falsifierThreshold_pos (product of two positives). Named bands come from named_redshift_falsifier_bands. Measurement separation is the lambda that applies measured_near_LCDM_not_RS_linear. The honest-scope field is fun _ => rfl.
why it matters
This is the master cert for Cosmology Track 4.C structural form: the algebraic discriminator that RS $w(z)$ differs from ΛCDM by a $\varphi^{-44}$-suppressed linear term. Downstream, darkEnergyWofZStructuralCert_inhabited simply witnesses Nonempty of the structure from this value, feeding the one-statement Track 4.C theorem.
Framework link: rung 44 is the same scale as baryogenesis $\eta_B = \varphi^{-44}$ on the $\varphi$-ladder (PhiRungLadder). The module status is structural theorem, zero sorry, zero RS-internal axiom. What remains open is the true FPT cosmic Z-aging functional form; the linear placeholder is explicitly a non-vacuous witness for the discriminator inequality, not the final dynamical prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.