module module moderate

`IndisputableMonolith.Cosmology.DarkEnergyWofZStructural`

Structural cosmology module fixing ΛCDM's constant dark-energy equation of state w = −1 against the Recognition Science linear w(z) built from φ^{−44}. It proves agreement at z = 0, strict separation for z > 0, and a positive falsifier threshold on the deviation. Cosmologists and the Planck/BAO/SNe likelihood attachment cite it. Content is definitions plus elementary algebraic identities on the φ-ladder.

claimThe module records the ΛCDM equation of state $w_{\Lambda\mathrm{CDM}}=-1$ (redshift-independent) and the RS linear model $w_{\mathrm{RS}}(z)$ built from the scale $\varphi^{-44}$. It proves $w_{\mathrm{RS}}(0)=w_{\Lambda\mathrm{CDM}}$, $w_{\mathrm{RS}}(z)\neq w_{\Lambda\mathrm{CDM}}$ for all $z>0$, and that the absolute deviation admits a strictly positive falsifier threshold.

background

Recognition Science places cosmological scales on the φ-ladder (the self-similar fixed point forced at T6). The companion module PhiRungLadder records baryon-asymmetry rungs and their factorizations through the eight-tick period. Constants supplies the RS-native tick τ₀. Dark energy is treated here only through its equation-of-state parameter w, not through a full Friedmann integration.

ΛCDM takes w identically −1 at every redshift. The RS structural ansatz is a linear tilt whose slope is set by the tiny ladder weight φ^{−44}. Because the tilt vanishes at z = 0, both models share the same present-day value; they peel apart only at positive redshift. The module therefore supplies a clean, parameter-light falsifier rather than a full dynamical DE sector.

proof idea

Definition layer first: name the constant ΛCDM value, the positive ladder weight φ^{−44}, and the linear RS map z ↦ w_RS(z). Equality-at-zero is immediate substitution. Distinctness for z > 0 is a one-line positivity argument on the slope term. Absolute-deviation and falsifier-threshold lemmas are elementary comparisons of real numbers (no analysis beyond ordered-field arithmetic). No differential equations or likelihood integrals appear; those live downstream.

why it matters in Recognition Science

Feeds the verification module DarkEnergyWPlanckLikelihood, which upgrades the §7 dark-energy w(z) falsifier row with a dataset-specific Planck/BAO/SNe likelihood-style certificate (structural theorem, zero sorry). Also imported by Foundation.MeasureForcing (T9 forced measure on recognition states) and by Gravity.MasterTheoremHandoffIntegration (fork-handoff receipt across stationarity, residual/Bianchi, many-body, and Page-capacity tracks). Inside the RS chain it supplies the concrete cosmological observable that links the φ-ladder arithmetic to late-time expansion data, without reopening T5–T8 uniqueness.

scope and limits

Does not derive w(z) from the Friedmann equations or a microphysical DE Lagrangian.
Does not fit cosmological parameters or compute χ² against Planck/BAO/SNe.
Does not claim the linear tilt is the unique RS-compatible w(z).
Does not address early-universe DE, modified gravity, or neutrino sectors.
Does not evaluate numerical φ^{−44} beyond positivity and algebraic use.

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