Cosmology Cosmic Zhistory Linear Accumulation Kernel

The dark-energy shape

Dark energy is the name cosmologists give to the observation that the universe's expansion is accelerating. In the standard cosmological model, this acceleration is described by an equation of state, a number usually written w, that relates the pressure of the mysterious substance to its energy density. The simplest possibility, a cosmological constant, has w exactly equal to -1. But measurements allow for a small deviation, and the question of how that deviation changes over cosmic time is an open problem in physics.

In the Recognition Science framework, the dark-energy deviation is not posited freely. The framework's Bosonic Identity Theorem provides a specific formula: the deviation at any redshift z equals a constant times the ratio of a quantity called cosmic Z-complexity at that redshift to its value today. This quantity, Z(z), is a measure of accumulated structural complexity in the universe. The framework proves a shape reduction theorem: the normalized dark-energy deviation is exactly equal to the normalized cosmic-Z history. This means the entire problem of the dark-energy shape is equivalent to the problem of deriving how Z accumulates.

The declaration linear_accumulation_kernel establishes a conditional result. If cosmic Z accumulates linearly in the scale factor, meaning Z(z) = Z_today / (1+z), then the framework's theorem proves that the dark-energy deviation takes the canonical form δw(z) = δw₀/(1+z). The machine-checked library of formal theorems verifies this derivation. The key equation is: w(z) = -1 + δw₀/(1+z). This is not a new prediction; it is the standard parametrization used in cosmological data analysis. What the framework contributes is a derivation of this shape from a single stated premise, rather than treating it as an arbitrary fitting function.

The theorem also establishes boundary conditions. Today, at z=0, the deviation equals its present value δw₀. In the early universe, as Z approaches zero, the deviation vanishes and the equation of state recovers exactly w = -1, the cosmological constant value. The framework's library proves these limits hold.

What the declaration does not claim is equally important. It does not prove that cosmic Z actually accumulates linearly in the scale factor. That remains a hypothesis, a physically motivated assumption about the nature of complexity growth. The theorem is conditional: if the premise holds, the shape follows. The framework is explicit that the accumulation law, whether linear in scale factor, linear in cosmic time, or some power law, is the single remaining freedom. The general reciprocal history theorem shows that any history of the form Z(z) = Z_today / g(z) produces a deviation δw(z) = δw₀ / g(z), so the choice of g is exactly the open question. This honest residue is the entire content of the dark-energy shape problem in this framework.

/-- **SHAPE REDUCTION.** The normalized dark-energy deviation equals the normalized
cosmic-Z history. Deriving the dark-energy shape is exactly deriving `Z(z)`. -/
theorem shape_reduction (dw0 Zt : ℝ) (Zhist : ℝ → ℝ) (z : ℝ) (hdw : dw0 ≠ 0) :
    bitDeviation dw0 Zt Zhist z / bitDeviation dw0 Zt Zhist 0
      = (Zhist z / Zt) / (Zhist 0 / Zt) := by
  rw [bitDeviation_eq, bitDeviation_eq, mul_div_mul_left _ _ hdw]

/-- **LINEAR ACCUMULATION FORCES THE CANONICAL KERNEL.** With the linear-`a` cosmic-Z
history, the BIT kernel produces exactly the canonical `δw(z) = δw₀/(1+z)` deviation. The
`1/(1+z)` shape is derived from the accumulation premise, not posited. -/
theorem linear_accumulation_forces_canonical_kernel (dw0 Zt z : ℝ)
    (hZt : Zt ≠ 0) (_hz : (1 : ℝ) + z ≠ 0) :
    bitDeviation dw0 Zt (linearZ Zt) z = dw0 / (1 + z) := by
  rw [bitDeviation_eq]
  unfold linearZ
  rw [div_div, mul_comm (1 + z) Zt, ← div_div, div_self hZt, mul_one_div]

/-- Today (`Z(0) = Z_today`), the deviation is `δw₀`. -/
theorem bitDeviation_today (dw0 Zt : ℝ) (Zhist : ℝ → ℝ)
    (h0 : Zhist 0 = Zt) (hZt : Zt ≠ 0) :
    bitDeviation dw0 Zt Zhist 0 = dw0 := by
  rw [bitDeviation_eq, h0, div_self hZt, mul_one]

/-- Early universe (`Z(z) = 0`): the deviation vanishes, recovering `w = -1`. -/
theorem bitKernel_early (dw0 Zt : ℝ) (Zhist : ℝ → ℝ) (z : ℝ) (h : Zhist z = 0) :
    bitKernel dw0 Zt Zhist z = -1 := by
  unfold bitKernel; rw [h]; simp

/-- **GENERAL RECIPROCAL HISTORY.** For any cosmic-Z history of reciprocal form
`Z(z) = Z_today / g(z)`, the BIT deviation is `δw(z) = δw₀ / g(z)`. The canonical kernel is
`g(z) = 1+z` (linear-in-`a`); a power-law history `g(z) = (1+z)^p` gives
`δw(z) = δw₀/(1+z)^p`, where the shape index `p` is read directly off the `w(z)`
reconstruction. The accumulation law chooses `g`; every downstream observable is then fixed.
This is the precise statement that U5's residue is exactly the choice of `g`. -/
theorem reciprocal_history_kernel (dw0 Zt : ℝ) (g : ℝ → ℝ) (z : ℝ) (hZt : Zt ≠ 0) :
    bitDeviation dw0 Zt (fun z => Zt / g z) z = dw0 / g z := by
  rw [bitDeviation_eq]
  show dw0 * (Zt / g z / Zt) = dw0 / g z
  rw [div_div, mul_comm (g z) Zt, ← div_div, div_self hZt, mul_one_div]

What this page does not claim

The theorem does not prove that cosmic Z accumulates linearly in the scale factor; that remains a hypothesis. The framework does not derive the value of the dark-energy deviation amplitude δw₀. The result does not claim that the canonical 1/(1+z) shape is the only possible dark-energy evolution, only that it follows from one specific premise.

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