Cosmology Cosmic Zscale Law Cosmic Zscale Law Cert

The scale-affine ledger law

In cosmology, the scale factor a(z) = 1/(1+z) measures how much the universe has expanded since light at redshift z was emitted. Today, at z = 0, it equals 1; at early times, as z grows large, it approaches 0. The dark-energy equation of state, often written w(z), describes how the pressure of dark energy relates to its density. A common parametrization writes w(z) = -1 + δw(z), where δw(z) is a small deviation from the cosmological constant value -1. The question is what shape that deviation takes as a function of redshift.

The Recognition Science framework answers this by introducing a condition it calls the scale-affine ledger law. The ledger, a discrete record of recognition events, is required to be uniform in the scale-factor coordinate: no intermediate scale-factor value is preferred over any other. Formally, the normalized accumulated cosmic-Z fraction Zfrac(a) must preserve convex interpolation between the early endpoint a=0, where Zfrac=0, and today a=1, where Zfrac=1. The statement is that for every a, Zfrac((1-a)·0 + a·1) = (1-a)·Zfrac(0) + a·Zfrac(1).

This single condition is enough. The machine-checked library of formal theorems proves that any function satisfying the scale-affine ledger law must equal the identity: Zfrac(a) = a. Consequently, the redshift history is forced to be Z(z) = Z_today/(1+z), and the dark-energy deviation takes the canonical form δw(z) = δw₀/(1+z). The equation of state becomes w(z) = -1 + δw₀/(1+z). The certificate CosmicZScaleLawCert packages these four forced results: the identity map, the linear redshift history, the canonical deviation, and the canonical kernel.

The status is precise. The theorem is conditional: it holds under the named scale-affine ledger admissibility law, which is an assumption, not a derived fact. The certificate proves that if the ledger is uniform in scale-factor coordinate, then the dark-energy shape follows. It does not prove that the ledger is in fact uniform, nor does it fit any curve to observational data. The condition is an admissibility statement about what the ledger may select, not a measurement of what it does select.

What the certificate does not claim is equally important. It does not claim that the scale-affine law is physically realized; that remains an open question about whether the ledger's uniformity holds in the actual universe. It does not claim any numerical agreement with supernova or cosmic microwave background observations. And it does not claim to derive the value of δw₀, which remains a free parameter in the framework. The certificate is a structural result: given the law, the shape follows. Whether the law holds is a separate matter, left for empirical test.

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

/-- Scale-affinity forces the redshift history to be the linear-in-scale-factor history
`Z(z)=Z_today/(1+z)`. -/
theorem scaleAffine_forces_linearZ (Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ) :
    ZfromScaleLaw Zt law z = CosmicZHistory.linearZ Zt z := by
  unfold ZfromScaleLaw CosmicZHistory.linearZ scaleFactor
  rw [scaleAffine_forces_identity law]
  rw [mul_one_div]

/-- Therefore scale-affinity forces the canonical BIT deviation
`δw(z)=δw₀/(1+z)`. -/
theorem scaleAffine_forces_canonical_deviation (dw0 Zt : ℝ) (law : ScaleAffineZLaw)
    (z : ℝ) (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
    CosmicZHistory.bitDeviation dw0 Zt (ZfromScaleLaw Zt law) z = dw0 / (1 + z) := by
  have hfun : ZfromScaleLaw Zt law = CosmicZHistory.linearZ Zt := by
    funext x
    exact scaleAffine_forces_linearZ Zt law x
  rw [hfun]
  exact CosmicZHistory.linear_accumulation_forces_canonical_kernel dw0 Zt z hZt hz

/-- The scale-law certificate is inhabited. -/
def cosmicZScaleLawCert : CosmicZScaleLawCert where
  identity_forced := scaleAffine_forces_identity
  redshift_history_forced := scaleAffine_forces_linearZ
  canonical_deviation_forced := scaleAffine_forces_canonical_deviation
  canonical_kernel_forced := scaleAffine_forces_canonical_kernel

/-- A normalized cosmic-Z history is scale-affine if it preserves the interpolation from
the early zero-complexity endpoint `a=0` to today `a=1`.

The field `scale_affine_from_early_to_today` is the precise no-extra-coordinate condition:
the ledger is uniform in the scale-factor coordinate until a further physical structure is
introduced. -/
structure ScaleAffineZLaw where
  /-- Normalized Z-fraction as a function of scale factor `a`. -/
  Zfrac : ℝ → ℝ
  /-- Early endpoint: no accumulated cosmic Z at `a=0`. -/
  early_zero : Zfrac 0 = 0
  /-- Today endpoint: normalized accumulated cosmic Z is `1` at `a=1`. -/
  today_one : Zfrac 1 = 1
  /-- Ledger-uniform interpolation between the two endpoints. -/
  scale_affine_from_early_to_today :
    ∀ a : ℝ, Zfrac ((1 - a) * 0 + a * 1) = (1 - a) * Zfrac 0 + a * Zfrac 1

What this page does not claim

The scale-affine ledger law is physically realized; it is an admissibility assumption, not a derived fact. Any numerical agreement with observational data on dark energy; no curve fitting is involved. The value of δw₀ is derived; it remains a free parameter in the framework. The scale-affine law holds at all redshifts; the theorem only covers the interval from a=0 to a=1.

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: