Cosmology Cosmic Zhistory Linear Z Antitone

The cosmic-Z history

In cosmology, redshift (the stretching of light from distant objects as the universe expands) is a direct measure of look-back time: higher redshift means earlier epochs. A proposed quantity called cosmic-Z complexity, written Z(z), is meant to track how much of some underlying structure has accumulated by the time the universe was at redshift z. Today, at z = 0, the accumulated amount is Z_today. The framework's library of machine-checked formal theorems defines one candidate history, called linearZ, by the rule Z(z) = Z_today / (1 + z). This is the simplest assumption: complexity accumulates in direct proportion to the scale factor a = 1/(1+z), so it grows smoothly as the universe expands.

The declaration linearZ_antitone proves a monotonicity property of this candidate history. The theorem states that for non-negative Z_today, and for any two redshifts z1 ≤ z2, the value at the larger redshift is no greater than the value at the smaller one: Z(z2) ≤ Z(z1). In plain language, the linear history is non-increasing in redshift. Because higher redshift means earlier times, this says the accumulated complexity was smaller in the past and has been growing toward its present value. The proof is a short algebraic argument using the fact that 1+z is positive and increasing in z, so its reciprocal is decreasing. This is a THEOREM: it is fully proved inside the machine-checked library, with no gaps or extra axioms.

The monotonicity result matters because of a separate, conditional derivation in the same module. The framework's BIT kernel defines the dark-energy equation of state as w(z) = -1 + δw₀ · Z(z)/Z_today, where δw₀ is the deviation from a cosmological constant today. A theorem called shape_reduction shows the normalized deviation equals the normalized Z-history. A further theorem, linear_accumulation_forces_canonical_kernel, proves that if the Z-history is the linear one defined above, then the deviation takes exactly the canonical form δw(z) = δw₀/(1+z). That is the familiar 1/(1+z) shape often posited in dark-energy models. The monotonicity of linearZ is a supporting property that makes this candidate history well-behaved: it is positive, starts at Z_today today, and declines monotonically into the past.

What linearZ_antitone does not claim is the premise itself. The theorem assumes the linear-in-scale-factor history; it does not derive why accumulation should be linear in a rather than in cosmic time or in some power a^p. That choice remains a HYPOTHESIS, explicitly named LinearScaleFactorAccumulation in the module. The monotonicity proof also assumes Z_today is non-negative and restricts to z ≥ 0, so it says nothing about negative redshifts (the future) or about a negative Z_today. The theorem is a clean property of one definition, not an observational statement about the actual universe.

The practical consequence is a sharpened statement of what remains open. The framework has reduced the dark-energy shape problem to a single question: why does Z accumulate linearly in the scale factor? If that premise is granted, the canonical 1/(1+z) deviation follows exactly, and linearZ_antitone confirms the history is monotone as a physical complexity measure should be. If the premise fails, the same shape_reduction theorem still holds, but the deviation shape would be different, for example δw₀/(1+z)^p for a power-law history. The monotonicity theorem is one brick in a wall that stands only if the foundation premise is accepted.

/-- The linear-`a` history is non-increasing in `z` (less Z accumulated at earlier epochs)
on `z ≥ 0`, for non-negative `Z_today`. -/
theorem linearZ_antitone (Zt : ℝ) (hZt : 0 ≤ Zt) {z1 z2 : ℝ}
    (h1 : 0 ≤ z1) (h12 : z1 ≤ z2) : linearZ Zt z2 ≤ linearZ Zt z1 := by
  unfold linearZ
  have hd1 : (0 : ℝ) < 1 + z1 := by linarith
  have hd2 : (0 : ℝ) < 1 + z2 := by linarith
  gcongr

/-- **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 linear-in-scale-factor accumulation premise itself is not derived; it remains a hypothesis. The monotonicity theorem does not apply to negative redshifts or to negative values of Z_today. The theorem makes no observational claim about the actual dark-energy equation of state in the universe.

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: