Encyclopedia Cosmology Cosmology Dark Energy Wof Zstructural W Rs Linear Distinct From Lcdm At Positive

ARTICLE 4 claims 3 theorems 1 model

Cosmology Dark Energy Wof Zstructural W Rs Linear Distinct From Lcdm At Positive

A machine-checked theorem states that a proposed dark-energy model must differ from the standard constant at any positive redshift, but the specific form of that difference remains an open hypothesis.

The structural discriminator

In cosmology, the dark-energy equation of state w(z) describes how the pressure of dark energy relates to its density as the universe expands. The standard ΛCDM model takes this to be a constant, w = -1, matching the simplest case of a cosmological constant. The Recognition Science framework proposes a different form, one that depends on redshift z, the measure of how much the universe has expanded since the light we see was emitted.

The framework's machine-checked library of formal theorems contains a declaration that pins down a structural consequence of this proposal. It states that for any positive redshift, the framework's linear placeholder w_RS(z) = -1 + φ⁻⁴⁴·z is strictly greater than -1. The number φ⁻⁴⁴, about 6.38 × 10⁻¹⁰, is a tiny positive constant that comes from the framework's internal rung-44 scale. The theorem proves that this difference is positive, not zero, at any redshift greater than zero.

This is a theorem about the algebraic structure, not a physical prediction. The framework's library proves that if the equation of state were exactly this linear function, it would be distinct from ΛCDM at any positive redshift. It also proves that any measurement of w that falls within a certain narrow band around -1 would be incompatible with this specific linear form. The band's width at a given redshift is exactly φ⁻⁴⁴·z.

In Recognition Science, this is called the structural discriminator. It exists to show that the framework's approach can produce a concrete, testable difference from the standard model. The specific functional form of the deviation, how w actually changes with redshift, is not derived. The linear placeholder is documented as a placeholder, a non-vacuous witness that the discriminator inequality can be satisfied. The real dynamics, the framework's FPT cosmic Z-aging story, remain future work.

What the declaration does not claim is as important as what it proves. It does not claim that the linear form is the true equation of state. It does not claim that the framework has derived the actual time-evolution of dark energy. It does not claim that the tiny deviation is currently measurable. The theorem only establishes a structural fact: a specific proposal differs from the standard constant at any positive redshift, and any measurement too close to -1 would rule that proposal out.

THEOREM w_RS_linear_distinct_from_LCDM_at_positive_z · IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean
w_RS_linear_distinct_from_LCDM_at_positive_z · IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean:126
/-- The structural discriminator: at positive redshift, the RS w(z)
value strictly exceeds the ΛCDM constant `-1` by the positive
amount `φ^{-44} · z`. -/
theorem w_RS_linear_distinct_from_LCDM_at_positive_z (z : ℝ) (h : 0 < z) :
    w_RS_linear z > w_LCDM_value := by
  unfold w_RS_linear w_LCDM_value
  have hphi : 0 < phi_neg_44 := phi_neg_44_pos
  have : 0 < phi_neg_44 * z := mul_pos hphi h
  linarith
THEOREM phi_neg_44_pos · IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean
theorem phi_neg_44_pos : 0 < phi_neg_44 := by
  unfold phi_neg_44
  exact zpow_pos phi_pos _
THEOREM measured_near_LCDM_not_RS_linear · IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean
measured_near_LCDM_not_RS_linear · IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean:180
/-- A measurement closer to ΛCDM than the RS structural separation
cannot equal the RS structural prediction. This is the formal falsifier
band used by the dataset row. -/
theorem measured_near_LCDM_not_RS_linear
    (z : ℝ) (h : 0 < z) {w_measured : ℝ}
    (hclose : |w_measured - w_LCDM_value| < falsifierThreshold z) :
    w_measured ≠ w_RS_linear z := by
  intro h_eq
  have hdist := w_RS_linear_abs_deviation_eq_threshold z (le_of_lt h)
  rw [h_eq] at hclose
  rw [hdist] at hclose
  exact (lt_irrefl (falsifierThreshold z)) hclose
MODEL w_RS_linear · IndisputableMonolith/Cosmology/DarkEnergyWofZStructural.lean
/-- A generic non-ΛCDM witness profile (NOT the RS dark-energy prediction).

`w_RS_linear z := -1 + φ^{-44} · z`

At `z = 0`, `w_RS_linear(0) = -1` (matches ΛCDM exactly). At positive
redshift, the deviation is `φ^{-44} · z`, positive.

HONESTY WARNING: this is **not** the RS dark-energy equation of state. Its slope
`φ^{-44} ≈ 6×10⁻¹⁰` is the baryogenesis `η_B` scale, not the dark-energy amplitude;
it is zero today and grows without bound into the past, which is the wrong sign and
scale for the cosmic-aging mechanism (whose deviation is maximal today and decays as
`1/(1+z)`). The correct RS shape is the antitone cosmic-aging kernel
`w(z) = -1 + δw₀/(1+z)`; its un-attenuated ceiling normalization `δw₀ = J(φ) ≈ 0.118`
lives in `Cosmology.DeltaWKernel.canonicalDeltaW` and
`Foundation.MaximalForcing.w_RS_kernel`, while the protocol-carried prediction of
record uses the attenuated `δw₀ = A_RS = φ⁻⁴·J(φ) ≈ 0.017`
(`Cosmology.DarkEnergyCPLPointForced`). `w_RS_linear` is retained only as a generic
witness for structural discriminator and carrier-independence arguments: it shows that
*some* upward-deviating profile distinct from exact ΛCDM exists. -/
noncomputable def w_RS_linear (z : ℝ) : ℝ :=
  -1 + phi_neg_44 * z

What this page does not claim

The linear form is not claimed to be the true equation of state; it is a placeholder. The framework has not derived the actual time-evolution of dark energy; that remains future work. The tiny deviation is not claimed to be currently measurable with existing instruments.

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/Cosmology/DarkEnergyWofZStructural.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND