Cosmology Cosmic Zscale Law Scale Factor Pos

The scale factor's positivity

In cosmology, the scale factor measures how much the universe has expanded since an early epoch. It is usually written as a function of redshift, the stretching of light from distant objects. The standard convention sets the scale factor to 1 today, so a value of 0.5 means the universe was half its current size when the light was emitted. The formula is a(z) = 1 / (1 + z), which gives 1 at z = 0 and approaches 0 as z grows without bound.

The Recognition Science framework's library, a machine-checked collection of formal theorems, contains a small result called scaleFactor_pos. It proves that for any redshift z greater than or equal to 0, the scale factor is strictly positive. This is a conditional statement: it holds only under the assumption that z is nonnegative, which is the physically meaningful range for cosmological observations. The proof is a direct algebraic consequence of the defining formula, not an empirical measurement or a new physical postulate.

Two companion theorems in the same module round out the picture. One, scaleFactor_today, states that the scale factor equals 1 at redshift 0, matching the convention that today is the reference point. The other, scaleFactor_le_one, proves that for z ≥ 0 the scale factor never exceeds 1. Together these three results pin down the basic shape: the scale factor starts at 1 today and decreases monotonically toward 0 as we look further back in time, but it never becomes negative or zero for any finite nonnegative redshift.

In Recognition Science, this positivity result is a stepping stone within a larger derivation about dark energy. The framework models cosmic history through a discrete recognition ledger, a record of events with a forced cost structure. A separate theorem, scaleAffine_forces_identity, shows that if the normalized cosmic-Z fraction preserves convex interpolation between the early endpoint a=0 and today a=1, then that fraction must equal the scale factor itself. This leads to the canonical dark-energy equation of state w(z) = -1 + δw₀/(1+z). The positivity theorem ensures that this construction is well-defined across the entire observable range of redshifts.

The scaleFactor_pos theorem does not claim that the universe actually obeys this specific scale factor. It establishes a mathematical fact about a conventional definition, conditional on the standard formula. Whether the real cosmos follows this exact relation is a separate empirical question. The theorem also does not assert anything about negative redshifts, which would correspond to future epochs in some coordinate choices; those are outside its stated assumption. And it says nothing about the physical mechanism driving expansion, only about the formal properties of the function used to describe it.

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

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

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

What this page does not claim

The theorem does not assert that the real universe follows this exact scale factor. The theorem says nothing about negative redshifts, which are outside its stated assumption. The theorem does not address the physical mechanism driving cosmic expansion.

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: