module module moderate

`IndisputableMonolith.Cosmology.DarkEnergyWofZStructural`

Structural module for the dark-energy equation of state w(z): ΛCDM is the constant w=-1, while RS supplies a linear-in-z model that equals -1 at z=0 and deviates at z>0 by a φ^{-44} scale. Cosmologists and RS verifiers cite it for the built-in falsifier threshold used against Planck/BAO/SNe. Content is definitional plus elementary algebraic identities and positivity facts.

claimΛCDM has constant equation of state $w_{\Lambda\mathrm{CDM}}=-1$. The RS linear model $w_{\mathrm{RS}}(z)$ satisfies $w_{\mathrm{RS}}(0)=-1$, coincides with ΛCDM at $z=0$, and is strictly distinct for $z>0$, with absolute deviation controlled by the positive scale $\varphi^{-44}$. A positive falsifier threshold bounds that deviation.

background

In standard FLRW cosmology the dark-energy equation of state $w=p/\rho$ is constant and equal to $-1$ for a pure cosmological constant (ΛCDM). Redshift dependence of $w(z)$ is therefore a clean observational discriminator.

Recognition Science places dimensionless scales on the $\varphi$-ladder (imported from the baryon-rung module and the RS constants). The structural small parameter appearing here is $\varphi^{-44}>0$. The module records both the classical constant $w=-1$ and an RS linear ansatz $w_{\mathrm{RS}}(z)$ engineered to match ΛCDM at $z=0$ while producing a controlled, falsifiable drift at positive redshift.

Upstream material is limited to the constants package (RS-native tick $\tau_0$) and the $\varphi$-ladder arithmetic; no dynamical field equations are solved in this file.

proof idea

Mostly a definition module. The ΛCDM value is introduced as the constant $-1$ and proved equal to $-1$ by reflexivity. The RS linear model is defined so that evaluation at $z=0$ recovers $-1$, hence equality with ΛCDM at the present epoch. Distinctness for $z>0$ and the absolute-deviation identity are pure algebra. Positivity of $\varphi^{-44}$ and of the falsifier threshold follow from positivity of powers of $\varphi>1$. No analytic estimates or measure theory are required.

why it matters in Recognition Science

Supplies the structural $w(z)$ objects consumed by the Planck/BAO/SNe likelihood attachment (Verification.DarkEnergyWPlanckLikelihood), which upgrades the dark-energy falsifier row to a dataset-specific certificate. Also imported into Foundation.MeasureForcing (T9 forced measure on recognition states) and the gravity master-theorem handoff integration, so the same $w$-comparison sits on both the cosmology-verification and the gravity-integration paths. Ties the DE sector to the $\varphi$-ladder and the eight-tick arithmetic without introducing new axioms.

scope and limits

Does not derive w(z) from Einstein equations or an RS action.
Does not fit cosmological data; only structural identities and a threshold.
Does not claim the linear RS ansatz is the unique RS prediction.
Does not bound higher-order redshift terms beyond the linear model.
Does not address early-universe or radiation-era equation of state.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.MeasureForcing module_import
IndisputableMonolith.Gravity.MasterTheoremHandoffIntegration module_import
IndisputableMonolith.Verification.DarkEnergyWPlanckLikelihood module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cosmology.PhiRungLadder module_import

declarations in this module (30)

def w_LCDM_value L78
theorem w_LCDM_value_eq_neg_one L80
def phi_neg_44 L87
theorem phi_neg_44_pos L89
def w_RS_linear L112
theorem w_RS_linear_at_zero L115
theorem w_RS_linear_eq_LCDM_at_zero L119
theorem w_RS_linear_distinct_from_LCDM_at_positive_z L127
theorem w_RS_linear_distinct_from_LCDM_abs L135
theorem w_RS_linear_deviation_magnitude L143
def falsifierThreshold L151
theorem falsifierThreshold_pos L155
theorem w_RS_linear_abs_deviation_eq_threshold L162
theorem LCDM_abs_deviation_from_w_RS_linear_eq_threshold L170
theorem measured_near_LCDM_not_RS_linear L181
theorem exact_LCDM_measurement_not_RS_linear L193
def redshift_half L201
def redshift_one L204
theorem redshift_half_pos L206
theorem redshift_one_pos L210
theorem w_RS_linear_at_redshift_half L215
theorem w_RS_linear_at_redshift_one L221
theorem falsifierThreshold_at_redshift_half L227
theorem falsifierThreshold_at_redshift_one L233
theorem named_redshift_falsifier_bands L239
theorem falsifier_band_at_redshift L255
structure DarkEnergyWofZStructuralCert L267
def darkEnergyWofZStructuralCert L292
theorem darkEnergyWofZStructuralCert_inhabited L305
theorem dark_energy_w_of_z_one_statement L323