Verification Dark Energy Wplanck Likelihood

The w0 consistency check

In cosmology, dark energy is often summarized by a single number w, the ratio of its pressure to its energy density. A value of exactly -1 means dark energy behaves like a cosmological constant, a fixed energy of empty space that does not change over time. The Planck 2018 satellite data, combined with baryon acoustic oscillations and supernova surveys, gives a constant-w fit of w0 = -1.03 ± 0.03.

The Recognition Science framework derives its own structural prediction for w at zero redshift: w_RS(0) = -1. This is not a fit to cosmological data; it follows from the framework's internal forcing chain. The module in question, a machine-checked library of formal theorems, compares this baseline against the measured central value. The absolute difference is 0.03, exactly equal to the quoted one-sigma uncertainty. The certificate proves this residual is less than or equal to that sigma, meaning the framework's baseline is within one standard deviation of the observed constant-w value.

The module also checks a second, more subtle prediction. Away from zero redshift, the framework expects deviations from w = -1 to scale as φ⁻⁴⁴ z, where φ is the golden ratio. At z = 1, this target scale is roughly 10⁻⁹, far smaller than the current measurement precision of 0.03. The theorem proves this target is below the one-sigma uncertainty, which means present surveys simply cannot detect such a tiny deviation. The dataset attachment is therefore explicitly marked as not currently sensitive to the framework's dynamic w(z) function.

What this establishes in plain language is a consistency check, not a confirmation. The framework's baseline value of -1 agrees with observation within the stated error bar, and its predicted deviation at higher redshift is too small for current instruments to see. The module assembles these facts into a single certificate object, with zero unproven assumptions and zero framework-specific axioms. It is a structural theorem about the framework's own predictions, not a new measurement of the cosmos.

The practical consequence is clear: the framework survives contact with the leading dark-energy dataset, but it does so precisely because it predicts nothing measurable beyond the cosmological constant at current precision. The dynamic part of the model, the w(z) function that would distinguish it from a pure constant, remains untested. That is the honest state of affairs, and the certificate is designed to say so explicitly.

/-- The RS z=0 baseline is within one sigma of the Planck+BAO+SNe constant-w result.
The residual equals the quoted sigma, so the statement is non-strict. -/
theorem darkEnergyW_residual_le_one_sigma :
    darkEnergyWResidual ≤ planckW0Sigma := by
  unfold darkEnergyWResidual planckW0Central rsW0Baseline planckW0Sigma
  rw [w_RS_linear_at_zero]
  norm_num

/-- Current `w` precision is not sensitive to the φ⁻⁴⁴ z-scale target. -/
theorem darkEnergyW_sigma_gt_rs_z1_target :
    rsW1DeviationTarget < planckW0Sigma := by
  unfold rsW1DeviationTarget darkEnergyWAttachment planckW0Sigma
  norm_num

/-- Dark-energy `w(z)` dataset attachment is present, positive, and
explicitly marked not currently sensitive. -/
theorem darkEnergyW_dataset_attachment_status :
    HasPositiveSensitivity darkEnergyWAttachment ∧
    HasPositiveTargetScale darkEnergyWAttachment ∧
    darkEnergyWAttachment.currentlySensitive = false :=
  ⟨darkEnergyW_sensitivity_pos, darkEnergyW_target_pos, rfl⟩

What this page does not claim

This module does not confirm the full dynamic RS w(z) function; it only tests the constant-w baseline. The agreement within one sigma does not prove the framework's derivation is physically correct. The φ⁻⁴⁴ z-scale target is a structural prediction, not a measured quantity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/DarkEnergyWPlanckLikelihood.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: