Cosmology Cosmic Zscale Law Scale Factor Today

The scale factor today

In cosmology, the scale factor tracks how distances in the universe grow with time. It is a number attached to each moment: at the Big Bang it is zero, today it is one, and in the future it will be larger. Astronomers usually write it as a function of redshift, the amount by which light from a distant galaxy has been stretched by the expansion of space. The standard relation is a(z) = 1 / (1 + z), where z is the redshift. A galaxy with redshift z = 1 emitted its light when the universe was half its current size; a galaxy with z = 2, when it was one third.

The machine-checked library of formal theorems in the Recognition Science framework records a small but exact fact about this relation. Its declaration scaleFactor_today proves that when the redshift is zero, the scale factor equals one: a(0) = 1. This is not a new physical discovery. It is the convention that defines the present epoch as the reference point. The same library also proves that for any nonnegative redshift, the scale factor stays between zero and one, which matches the ordinary meaning of the formula: looking back in time means seeing a smaller universe.

In Recognition Science, this convention sits inside a larger argument about dark energy. The framework models a cosmic ledger, a discrete record of events, and proposes that the dark-energy equation of state takes the form w(z) = -1 + δw₀/(1+z). The scale factor provides the coordinate for that history. A condition called the scale-affine ledger law states that equal fractions of the scale factor carry equal fractions of the accumulated ledger between the early universe and today. Under that law, the normalized history is forced to be exactly the scale factor itself, and the dark-energy shape follows.

The framework's library proves this forcing chain as a theorem conditional on the named admissibility law. The law is a definitional choice, not a derived result. The scale factor being one today is a convention that any cosmological framework adopts, and the Recognition Science library states it cleanly without adding physical content to that convention.

/-- The scale factor is `1` today. -/
theorem scaleFactor_today : scaleFactor 0 = 1 := by
  unfold scaleFactor
  norm_num

/-- For `z ≥ 0`, the scale factor is positive. -/
theorem scaleFactor_pos {z : ℝ} (hz : 0 ≤ z) : 0 < scaleFactor z := by
  unfold scaleFactor
  have h : (0 : ℝ) < 1 + z := by linarith
  positivity

/-- For `z ≥ 0`, the scale factor is at most `1`. -/
theorem scaleFactor_le_one {z : ℝ} (hz : 0 ≤ z) : scaleFactor z ≤ 1 := by
  unfold scaleFactor
  have h : (0 : ℝ) < 1 + z := by linarith
  rw [div_le_one h]
  linarith

/-- The scale-affine ledger law uniquely forces the normalized Z-fraction to be the identity
map on scale factor. -/
theorem scaleAffine_forces_identity (law : ScaleAffineZLaw) (a : ℝ) :
    law.Zfrac a = a := by
  have h := law.scale_affine_from_early_to_today a
  simpa [law.early_zero, law.today_one] using h

/-- The induced equation of state is the canonical kernel
`w(z)=-1+δw₀/(1+z)`. -/
theorem scaleAffine_forces_canonical_kernel (dw0 Zt : ℝ) (law : ScaleAffineZLaw)
    (z : ℝ) (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
    CosmicZHistory.bitKernel dw0 Zt (ZfromScaleLaw Zt law) z = -1 + dw0 / (1 + z) := by
  have h := scaleAffine_forces_canonical_deviation dw0 Zt law z hZt hz
  unfold CosmicZHistory.bitDeviation at h
  linarith [h]

What this page does not claim

The scale-affine ledger law is not derived from more basic principles; it is a named admissibility condition. The framework does not claim that the scale factor being one today is a physical discovery rather than a convention. No claim is made that the dark-energy equation of state w(z) = -1 + δw₀/(1+z) matches observational data.

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