Cosmology Cosmic Zhistory Bit Deviation Today

The today boundary

In cosmology, redshift z measures how much the universe has expanded since light left a distant object: z = 0 is today, z = 1 is when the universe was half its current size, and larger z means further back in time. The dark-energy equation of state, written w(z), describes how the pressure of dark energy relates to its density at each redshift. In the standard cosmological model, w = -1 exactly, a value called the cosmological constant. Observations allow small deviations from this value, and the question of how such a deviation would evolve with redshift is what the Recognition Science framework addresses.

The declaration bitDeviation_today establishes a boundary condition: at redshift zero, the deviation from the cosmological constant equals a fixed value, written δw₀. The theorem proves that if the cosmic-Z complexity, a measure of accumulated recognition events in the framework, has its today value Z_today, then the deviation today is exactly δw₀. This is a consistency check, a statement that the framework's definition of the deviation reduces to its own parameter at the present epoch. The proof is a short algebraic identity, verified in the machine-checked library of formal theorems.

The theorem does not claim what the value of δw₀ is. It does not claim how the deviation changes at any other redshift. It does not claim that the cosmic-Z complexity actually accumulates in any particular way. The declaration is a boundary condition, not a prediction. It says: if you know the deviation today, then at z = 0 the formula gives you back that same number. That is all.

In Recognition Science, this boundary condition is part of a larger reduction. The framework proves that the normalized deviation at any redshift equals the normalized cosmic-Z history. This is a theorem: the shape of the dark-energy deviation is exactly the shape of the cosmic-Z accumulation, no more and no less. The remaining freedom is the accumulation law itself. If cosmic Z accumulates linearly in the scale factor, the framework derives the canonical 1/(1+z) deviation. But why that linear accumulation should hold, rather than some other law, is not derived. That is the honest residue, an open question.

For a reader, the practical takeaway is this: the framework has a precise, machine-checked statement about the present value of the dark-energy deviation, and it is a boundary condition, not a prediction. The interesting physics, the shape of the deviation across cosmic history, is reduced to a single question about how cosmic complexity accumulates. That question remains open, and it is the target of future work.

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

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

What this page does not claim

The value of δw₀ is not derived or predicted by the theorem. The theorem does not establish how the deviation evolves at any redshift other than zero. The linear accumulation law is a hypothesis, not a consequence of the framework.

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: