Cosmology Cosmic Zhistory Bit Deviation Eq

The shape of dark energy

Dark energy is the name astronomers give to the unknown force that is speeding up the expansion of the universe. Its strength is not constant in the standard picture; it changes with time, and cosmologists describe that change with a number called the equation of state, written w(z). When w(z) equals -1, dark energy behaves like a simple cosmological constant, the energy of empty space. When w(z) is greater than -1, the force weakens as the universe ages. The deviation from -1, written δw(z), is the quantity that carries the shape of this change.

In the Recognition Science framework, the deviation has a specific form. The framework models dark energy as the result of a cosmic ledger, a discrete record of recognition events accumulated over the universe's history. The total amount recorded at redshift z is written Z(z), and its value today is Z_today. The framework's declaration bitDeviation_eq proves that the deviation at any time equals today's deviation δw₀ multiplied by the ratio Z(z)/Z_today. In plain terms, the shape of dark energy's weakness is exactly the shape of the universe's accumulated memory, no more and no less. This is a proved theorem in the machine-checked library of formal theorems, tagged THEOREM.

The same library proves two boundary facts. Today, when Z(0) equals Z_today, the deviation is exactly δw₀. In the early universe, when Z(z) is zero, the deviation vanishes and w(z) returns to -1, recovering the cosmological constant. These are also proved theorems. The framework then shows that if the accumulated memory grows linearly with the scale factor, meaning Z(z) = Z_today/(1+z), the deviation takes the canonical form δw(z) = δw₀/(1+z). This conditional derivation is a theorem, but it rests on the linear-accumulation premise, which is a HYPOTHESIS.

What bitDeviation_eq does not claim is that the linear accumulation law is true. The theorem proves a relationship between the deviation and the memory function, and it proves that linear growth produces the standard shape. It does not prove why the memory accumulates linearly in the scale factor rather than in cosmic time or some other power. That single question, the choice of the accumulation law, is the honest residue of the dark-energy shape problem. The framework has reduced the mystery to one stated premise, but it has not eliminated the premise.

/-- The deviation equals `δw₀ · Z(z)/Z_today`. -/
theorem bitDeviation_eq (dw0 Zt : ℝ) (Zhist : ℝ → ℝ) (z : ℝ) :
    bitDeviation dw0 Zt Zhist z = dw0 * (Zhist z / Zt) := by
  unfold bitDeviation bitKernel; ring

/-- 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

/-- **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]

What this page does not claim

The linear accumulation law is not proved; it is a stated hypothesis. The framework does not derive the value of today's deviation δw₀. No claim is made that the cosmic ledger is a physical object rather than a mathematical model.

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: