Cosmology Dark Energy Eos W Eq Neg One

The constant vacuum

In cosmology, dark energy is usually modeled by an equation of state parameter w, the ratio of its pressure to its energy density. The simplest model, the cosmological constant, has w = -1 exactly. In Recognition Science, a framework that derives physical structure from a discrete ledger of recognition events, a theorem named w_eq_neg_one derives this same value from a single structural assumption: the vacuum is phase-locked, meaning its recognition state is committed and does not update with the tick counter.

The derivation is short. A phase-locked mode has a committed ledger entry at x = 1, where the recognition cost J(1) = 0 is tick-independent. A constant energy density, one that does not change with volume, must satisfy the relativistic relation p = -ρ, giving w = p/ρ = -1. The theorem is proved in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms.

What the theorem does not claim is just as important. It does not claim that dark energy is a cosmological constant in the sense of a bare geometric term in Einstein's equations. It does not predict the measured value of w from first principles; it derives the value -1 conditional on the phase-locked assumption, which is itself a modeling choice. The theorem also does not address the cosmological constant problem, the enormous mismatch between the observed vacuum energy density and quantum field theory estimates. Those questions remain open.

Within the framework, the result replaces a definitional choice with a derived consequence: instead of setting w := -1 by hand, the framework proves it from the phase-locked structure. That is a step toward showing that the cosmological constant is not an arbitrary parameter but a forced outcome of the recognition ledger. The broader physical bridge, connecting the ledger to actual spacetime geometry, is still an open target.

/-- A phase-locked mode has a committed ledger entry at x = 1.
    Its J-cost is zero and does not change with the tick counter. -/
structure PhaseLocked where
  ratio : ℝ
  at_vacuum : ratio = 1
  cost_zero : Jcost ratio = 0

/-- Phase-locked modes exist: x = 1 has J(1) = 0. -/
def vacuum_mode : PhaseLocked where
  ratio := 1
  at_vacuum := rfl
  cost_zero := Jcost_unit0

/-- **THEOREM (w = -1)**: A constant energy density has w = -1.

    Proof: w = p/ρ. For a Lorentz-invariant constant energy density,
    the stress-energy tensor is T_μν = -ρ·g_μν (proportional to the
    metric). Therefore p = -ρ and w = p/ρ = -ρ/ρ = -1.

    In the ledger picture: phase-locked modes have J(1) = 0 at every
    tick. Their energy is the mode energy E_coh/16, which is the same
    at every lattice site (translation symmetry) and at every tick
    (phase locking). A spatially uniform, temporally constant energy
    density in GR has w = -1 identically. -/
theorem w_eq_neg_one (c : ConstantEnergyContribution) :
    equation_of_state c = -1 := by
  unfold equation_of_state
  rw [neg_div, div_self (ne_of_gt c.energy_pos)]

/-- The dark energy equation of state is exactly -1. -/
theorem dark_energy_w_derived :
    ∀ c : ConstantEnergyContribution, equation_of_state c = -1 :=
  w_eq_neg_one

What this page does not claim

The theorem does not predict the measured value of w from first principles. It does not claim dark energy is a bare geometric term in Einstein's equations. It does not address the cosmological constant problem.

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/DarkEnergyEOS.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: