Cosmology Dark Energy Equation Of State Depth Delta Bound

The delta bound

In cosmology, the dark energy equation of state is a function w(z) that describes how the pressure of dark energy relates to its density as the universe expands. The simplest model, ΛCDM, sets w = -1 exactly, meaning dark energy behaves like a constant energy density, the cosmological constant. More flexible models allow w to drift with redshift z, and the framework called Recognition Science organizes these possibilities into a finite set of five canonical models: ΛCDM, wCDM, the CPL parametrization, quintessence, and phantom. This is a definitional choice, not a physical derivation; the framework's machine-checked library of formal theorems merely counts these five models and proves that there are exactly five of them.

Within this framework, the declaration deltaBound defines a specific number: deltaBound = 1 / phi^5, where phi is the golden ratio, approximately 1.618. Using the identity phi^5 = 5*phi + 3, the framework proves that deltaBound is positive and that it is less than 0.1. In plain terms, this means deltaBound is about 0.09. The framework then uses this number as an upper limit on the deviation delta in a canonical model where w(z) = -1 + delta. So the declaration establishes that, in this particular model, the equation of state can deviate from -1 by at most about 0.09. This is a definition of a bound, not a measurement of the actual deviation.

The framework's library proves the arithmetic facts about deltaBound: that it is positive and that it is small, both as formal theorems. These proofs rely only on the definition of the golden ratio and basic inequalities. The declaration itself is a definition, so claims about it are tagged MODEL, not THEOREM. The framework does not claim that the actual dark energy equation of state in our universe has this bound, nor does it claim that the deviation is exactly 0.09. It only defines a candidate bound and proves its mathematical properties. The physical question of whether this bound matches observations remains entirely open.

What the declaration does not claim is worth stating plainly. It does not claim that w(z) actually equals -1 + delta for any observed dark energy. It does not claim that the five models are the only possible models of dark energy. And it does not claim that deltaBound is derived from the framework's forcing chain; it is simply a definition introduced for this specific model. The bound is a proposed constraint, not a prediction with a named falsifier. A reader should understand it as a mathematical object with proven properties, not as an empirical result.

/-- δ bound = 1/φ⁵. Using φ⁵ = 5φ + 3. -/
noncomputable def deltaBound : ℝ := 1 / phi ^ 5

theorem deltaBound_pos : 0 < deltaBound := by
  unfold deltaBound
  exact div_pos one_pos (pow_pos phi_pos 5)

theorem deltaBound_small : deltaBound < 0.1 := by
  unfold deltaBound
  have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
  rw [h5]
  have h_phi_gt : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  have h_denom : (11.05 : ℝ) < 5 * phi + 3 := by linarith
  have h_denom_pos : (0 : ℝ) < 5 * phi + 3 := by linarith
  rw [div_lt_iff₀ h_denom_pos]
  nlinarith

inductive DarkEnergyModel where
  | lambdaCDM
  | wCDM
  | w0wa_CPL
  | quintessence
  | phantom
  deriving DecidableEq, Repr, BEq, Fintype

theorem darkEnergyModel_count : Fintype.card DarkEnergyModel = 5 := by decide

What this page does not claim

The declaration does not claim that the actual dark energy equation of state in our universe has this bound. The declaration does not claim that the deviation delta is exactly 0.09. The declaration does not claim that the five models are the only possible models of dark energy.

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