IndisputableMonolith.Cosmology.DarkEnergyScaleAffinityDerivation

   1import Mathlib
   2import IndisputableMonolith.Cosmology.CosmicZScaleLaw
   3
   4/-!
   5# Dark-Energy Scale-Affinity Derivation
   6
   7This module tightens the remaining U5 residue.
   8
   9`CosmicZScaleLaw` proved:
  10
  11`ScaleAffineZLaw -> Z(z)/Z_today = a(z) -> δw(z)=δw0/(1+z)`.
  12
  13The remaining question was where `ScaleAffineZLaw` comes from. This module introduces the
  14lower admissibility principle that expresses the RS "no hidden coordinate" condition on the
  15cosmic scale interval:
  16
  17**NoHiddenScaleCoordinate.** Once the early endpoint `a=0` and the today endpoint `a=1`
  18are fixed, the recognition ledger may not insert an extra preferred coordinate inside the
  19interval. Therefore the normalized Z-fraction must preserve endpoint convex interpolation.
  20
  21That condition is exactly the scale-affine law, and Lean proves the conversion. This is the
  22strongest honest theorem-layer closure: the canonical shape is forced by the no-hidden-scale
  23coordinate admissibility condition. The remaining deeper problem, if desired, is to derive
  24that admissibility condition from the universal forcing layer rather than stating it as the
  25cosmic-Z admissibility gate.
  26
  27Status: THEOREM conditional on the named no-hidden-scale-coordinate admissibility gate.
  28Zero `sorry`, zero new `axiom`.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Cosmology
  33namespace DarkEnergyScaleAffinityDerivation
  34
  35noncomputable section
  36
  37/-! ## §1. No-hidden-scale-coordinate admissibility -/
  38
  39/-- The lower admissibility condition behind `ScaleAffineZLaw`.
  40
  41Interpretation: with only the early endpoint `a=0` and today endpoint `a=1` available, a
  42normalized ledger fraction cannot choose a nonlinear coordinate without adding extra
  43structure. Therefore it preserves endpoint interpolation. -/
  44structure NoHiddenScaleCoordinate where
  45  /-- Normalized Z-fraction as a function of scale factor. -/
  46  Zfrac : ℝ → ℝ
  47  /-- Early endpoint: no accumulated cosmic Z at `a=0`. -/
  48  early_zero : Zfrac 0 = 0
  49  /-- Today endpoint: normalized accumulated cosmic Z is `1` at `a=1`. -/
  50  today_one : Zfrac 1 = 1
  51  /-- No hidden coordinate: endpoint convex interpolation is preserved. -/
  52  no_hidden_coordinate :
  53    ∀ a : ℝ, Zfrac ((1 - a) * 0 + a * 1) = (1 - a) * Zfrac 0 + a * Zfrac 1
  54
  55/-- `NoHiddenScaleCoordinate` is exactly the data needed for `ScaleAffineZLaw`. -/
  56def noHidden_to_scaleAffine (H : NoHiddenScaleCoordinate) :
  57    CosmicZScaleLaw.ScaleAffineZLaw where
  58  Zfrac := H.Zfrac
  59  early_zero := H.early_zero
  60  today_one := H.today_one
  61  scale_affine_from_early_to_today := H.no_hidden_coordinate
  62
  63/-- The no-hidden-scale-coordinate condition forces normalized Z-fraction to be the scale
  64factor itself. -/
  65theorem noHidden_forces_identity (H : NoHiddenScaleCoordinate) (a : ℝ) :
  66    H.Zfrac a = a := by
  67  exact CosmicZScaleLaw.scaleAffine_forces_identity (noHidden_to_scaleAffine H) a
  68
  69/-- The no-hidden-scale-coordinate condition forces the redshift history
  70`Z(z)=Z_today/(1+z)`. -/
  71theorem noHidden_forces_linearZ (Zt : ℝ) (H : NoHiddenScaleCoordinate) (z : ℝ) :
  72    CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H) z =
  73      CosmicZHistory.linearZ Zt z :=
  74  CosmicZScaleLaw.scaleAffine_forces_linearZ Zt (noHidden_to_scaleAffine H) z
  75
  76/-- The no-hidden-scale-coordinate condition forces the canonical dark-energy deviation. -/
  77theorem noHidden_forces_canonical_deviation (dw0 Zt : ℝ)
  78    (H : NoHiddenScaleCoordinate) (z : ℝ)
  79    (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
  80    CosmicZHistory.bitDeviation dw0 Zt
  81        (CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H)) z =
  82      dw0 / (1 + z) :=
  83  CosmicZScaleLaw.scaleAffine_forces_canonical_deviation
  84    dw0 Zt (noHidden_to_scaleAffine H) z hZt hz
  85
  86/-- The no-hidden-scale-coordinate condition forces the canonical equation of state. -/
  87theorem noHidden_forces_canonical_kernel (dw0 Zt : ℝ)
  88    (H : NoHiddenScaleCoordinate) (z : ℝ)
  89    (hZt : Zt ≠ 0) (hz : (1 : ℝ) + z ≠ 0) :
  90    CosmicZHistory.bitKernel dw0 Zt
  91        (CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H)) z =
  92      -1 + dw0 / (1 + z) :=
  93  CosmicZScaleLaw.scaleAffine_forces_canonical_kernel
  94    dw0 Zt (noHidden_to_scaleAffine H) z hZt hz
  95
  96/-! ## §2. Canonical witness and certificate -/
  97
  98/-- The canonical no-hidden-coordinate law is inhabited by the identity Z-fraction. -/
  99def canonicalNoHiddenScaleCoordinate : NoHiddenScaleCoordinate where
 100  Zfrac := fun a => a
 101  early_zero := rfl
 102  today_one := rfl
 103  no_hidden_coordinate := by
 104    intro a
 105    ring
 106
 107/-- The canonical no-hidden-coordinate law maps to the canonical scale-affine law. -/
 108theorem canonicalNoHidden_maps_to_canonical :
 109    (noHidden_to_scaleAffine canonicalNoHiddenScaleCoordinate).Zfrac =
 110      CosmicZScaleLaw.canonicalScaleAffineZLaw.Zfrac := by
 111  rfl
 112
 113/-- **SCALE-AFFINITY DERIVATION CERTIFICATE.** The no-hidden-scale-coordinate admissibility
 114gate derives the scale-affine law and hence the canonical dark-energy shape. -/
 115structure ScaleAffinityDerivationCert where
 116  to_scale_affine :
 117    NoHiddenScaleCoordinate → CosmicZScaleLaw.ScaleAffineZLaw
 118  identity_forced :
 119    ∀ (H : NoHiddenScaleCoordinate) (a : ℝ), H.Zfrac a = a
 120  linearZ_forced :
 121    ∀ (Zt : ℝ) (H : NoHiddenScaleCoordinate) (z : ℝ),
 122      CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H) z =
 123        CosmicZHistory.linearZ Zt z
 124  canonical_deviation_forced :
 125    ∀ (dw0 Zt : ℝ) (H : NoHiddenScaleCoordinate) (z : ℝ),
 126      Zt ≠ 0 → (1 : ℝ) + z ≠ 0 →
 127        CosmicZHistory.bitDeviation dw0 Zt
 128            (CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H)) z =
 129          dw0 / (1 + z)
 130  canonical_kernel_forced :
 131    ∀ (dw0 Zt : ℝ) (H : NoHiddenScaleCoordinate) (z : ℝ),
 132      Zt ≠ 0 → (1 : ℝ) + z ≠ 0 →
 133        CosmicZHistory.bitKernel dw0 Zt
 134            (CosmicZScaleLaw.ZfromScaleLaw Zt (noHidden_to_scaleAffine H)) z =
 135          -1 + dw0 / (1 + z)
 136
 137/-- The scale-affinity derivation certificate is inhabited. -/
 138def scaleAffinityDerivationCert : ScaleAffinityDerivationCert where
 139  to_scale_affine := noHidden_to_scaleAffine
 140  identity_forced := noHidden_forces_identity
 141  linearZ_forced := noHidden_forces_linearZ
 142  canonical_deviation_forced := noHidden_forces_canonical_deviation
 143  canonical_kernel_forced := noHidden_forces_canonical_kernel
 144
 145end
 146
 147end DarkEnergyScaleAffinityDerivation
 148end Cosmology
 149end IndisputableMonolith
 150