IndisputableMonolith.Cosmology.CosmicZScaleLaw

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.Cosmology.CosmicZHistory
   5
   6/-!
   7# Cosmic Z Scale Law
   8
   9This module tightens the last shape residue in the dark-energy plan.
  10
  11`CosmicZHistory` proves that, under the BIT kernel,
  12
  13`δw(z) = δw₀ · Z(z)/Z_today`.
  14
  15So the dark-energy shape is exactly the normalized cosmic-Z history. The remaining question
  16is why that normalized history should be the scale factor `a(z)=1/(1+z)`.
  17
  18This module records the sharp admissibility condition that forces it:
  19
  20**Scale-affine ledger law.** Along the cosmic interval from the early zero-complexity
  21endpoint `a=0` to today `a=1`, equal scale-factor fractions carry equal recognition-ledger
  22fractions. Formally, the normalized Z-fraction preserves convex interpolation between the
  23two endpoints.
  24
  25That condition is not a curve fit. It is the statement that no intermediate scale-factor
  26coordinate is selected by the ledger before a new physical input is supplied. Under that
  27law, the normalized Z-history is uniquely `Z/Z_today = a`, and the BIT kernel gives
  28`δw(z)=δw₀/(1+z)`.
  29
  30Status: THEOREM conditional on the named scale-affine ledger admissibility law. Zero `sorry`,
  31zero new `axiom`.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Cosmology
  36namespace CosmicZScaleLaw
  37
  38open Constants
  39open Cost
  40
  41noncomputable section
  42
  43/-! ## §1. Scale-factor coordinate -/
  44
  45/-- The cosmological scale factor as a function of redshift. -/
  46def scaleFactor (z : ℝ) : ℝ := 1 / (1 + z)
  47
  48/-- The scale factor is `1` today. -/
  49theorem scaleFactor_today : scaleFactor 0 = 1 := by
  50  unfold scaleFactor
  51  norm_num
  52
  53/-- For `z ≥ 0`, the scale factor is positive. -/
  54theorem scaleFactor_pos {z : ℝ} (hz : 0 ≤ z) : 0 < scaleFactor z := by
  55  unfold scaleFactor
  56  have h : (0 : ℝ) < 1 + z := by linarith
  57  positivity
  58
  59/-- For `z ≥ 0`, the scale factor is at most `1`. -/
  60theorem scaleFactor_le_one {z : ℝ} (hz : 0 ≤ z) : scaleFactor z ≤ 1 := by
  61  unfold scaleFactor
  62  have h : (0 : ℝ) < 1 + z := by linarith
  63  rw [div_le_one h]
  64  linarith
  65
  66/-! ## §2. The scale-affine ledger law -/
  67
  68/-- A normalized cosmic-Z history is scale-affine if it preserves the interpolation from
  69the early zero-complexity endpoint `a=0` to today `a=1`.
  70
  71The field `scale_affine_from_early_to_today` is the precise no-extra-coordinate condition:
  72the ledger is uniform in the scale-factor coordinate until a further physical structure is
  73introduced. -/
  74structure ScaleAffineZLaw where
  75  /-- Normalized Z-fraction as a function of scale factor `a`. -/
  76  Zfrac : ℝ → ℝ
  77  /-- Early endpoint: no accumulated cosmic Z at `a=0`. -/
  78  early_zero : Zfrac 0 = 0
  79  /-- Today endpoint: normalized accumulated cosmic Z is `1` at `a=1`. -/
  80  today_one : Zfrac 1 = 1
  81  /-- Ledger-uniform interpolation between the two endpoints. -/
  82  scale_affine_from_early_to_today :
  83    ∀ a : ℝ, Zfrac ((1 - a) * 0 + a * 1) = (1 - a) * Zfrac 0 + a * Zfrac 1
  84
  85/-- The scale-affine ledger law uniquely forces the normalized Z-fraction to be the identity
  86map on scale factor. -/
  87theorem scaleAffine_forces_identity (law : ScaleAffineZLaw) (a : ℝ) :
  88    law.Zfrac a = a := by
  89  have h := law.scale_affine_from_early_to_today a
  90  simpa [law.early_zero, law.today_one] using h
  91
  92/-- The canonical scale-affine law, included as the witness that the admissibility class is
  93inhabited. -/
  94def canonicalScaleAffineZLaw : ScaleAffineZLaw where
  95  Zfrac := fun a => a
  96  early_zero := rfl
  97  today_one := rfl
  98  scale_affine_from_early_to_today := by
  99    intro a
 100    ring
 101
 102/-! ## §3. Redshift history forced by scale-affinity -/
 103
 104/-- The cosmic-Z history generated by a scale-affine law. -/
 105def ZfromScaleLaw (Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ) : ℝ :=
 106  Zt * law.Zfrac (scaleFactor z)
 107
 108/-- Scale-affinity forces the redshift history to be the linear-in-scale-factor history
 109`Z(z)=Z_today/(1+z)`. -/
 110theorem scaleAffine_forces_linearZ (Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ) :
 111    ZfromScaleLaw Zt law z = CosmicZHistory.linearZ Zt z := by
 112  unfold ZfromScaleLaw CosmicZHistory.linearZ scaleFactor
 113  rw [scaleAffine_forces_identity law]
 114  rw [mul_one_div]
 115
 116/-- Therefore scale-affinity forces the canonical BIT deviation
 117`δw(z)=δw₀/(1+z)`. -/
 118theorem scaleAffine_forces_canonical_deviation (dw0 Zt : ℝ) (law : ScaleAffineZLaw)
 119    (z : ℝ) (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
 120    CosmicZHistory.bitDeviation dw0 Zt (ZfromScaleLaw Zt law) z = dw0 / (1 + z) := by
 121  have hfun : ZfromScaleLaw Zt law = CosmicZHistory.linearZ Zt := by
 122    funext x
 123    exact scaleAffine_forces_linearZ Zt law x
 124  rw [hfun]
 125  exact CosmicZHistory.linear_accumulation_forces_canonical_kernel dw0 Zt z hZt hz
 126
 127/-- The induced equation of state is the canonical kernel
 128`w(z)=-1+δw₀/(1+z)`. -/
 129theorem scaleAffine_forces_canonical_kernel (dw0 Zt : ℝ) (law : ScaleAffineZLaw)
 130    (z : ℝ) (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
 131    CosmicZHistory.bitKernel dw0 Zt (ZfromScaleLaw Zt law) z = -1 + dw0 / (1 + z) := by
 132  have h := scaleAffine_forces_canonical_deviation dw0 Zt law z hZt hz
 133  unfold CosmicZHistory.bitDeviation at h
 134  linarith [h]
 135
 136/-! ## §4. Certificate -/
 137
 138/-- **COSMIC Z SCALE-LAW CERTIFICATE.** The named scale-affine ledger admissibility law
 139forces the normalized cosmic-Z history to be the scale factor and hence forces the canonical
 140dark-energy shape. -/
 141structure CosmicZScaleLawCert where
 142  identity_forced :
 143    ∀ (law : ScaleAffineZLaw) (a : ℝ), law.Zfrac a = a
 144  redshift_history_forced :
 145    ∀ (Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ),
 146      ZfromScaleLaw Zt law z = CosmicZHistory.linearZ Zt z
 147  canonical_deviation_forced :
 148    ∀ (dw0 Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ),
 149      Zt ≠ 0 → (1 : ℝ) + z ≠ 0 →
 150        CosmicZHistory.bitDeviation dw0 Zt (ZfromScaleLaw Zt law) z = dw0 / (1 + z)
 151  canonical_kernel_forced :
 152    ∀ (dw0 Zt : ℝ) (law : ScaleAffineZLaw) (z : ℝ),
 153      Zt ≠ 0 → (1 : ℝ) + z ≠ 0 →
 154        CosmicZHistory.bitKernel dw0 Zt (ZfromScaleLaw Zt law) z = -1 + dw0 / (1 + z)
 155
 156/-- The scale-law certificate is inhabited. -/
 157def cosmicZScaleLawCert : CosmicZScaleLawCert where
 158  identity_forced := scaleAffine_forces_identity
 159  redshift_history_forced := scaleAffine_forces_linearZ
 160  canonical_deviation_forced := scaleAffine_forces_canonical_deviation
 161  canonical_kernel_forced := scaleAffine_forces_canonical_kernel
 162
 163end
 164
 165end CosmicZScaleLaw
 166end Cosmology
 167end IndisputableMonolith
 168