IndisputableMonolith.ILG.GrowthODE

   1import Mathlib
   2import IndisputableMonolith.ILG.Kernel
   3import IndisputableMonolith.ILG.Reciprocity
   4
   5namespace IndisputableMonolith
   6namespace ILG
   7
   8open Real
   9
  10/-- The prefactor for the first-order ILG growth correction in EdS background.
  11    Derived from plugging D = a(1 + B a^alpha) into the growth ODE. -/
  12noncomputable def growth_prefactor (alpha C : ℝ) : ℝ :=
  13  (3 * C) / (2 * alpha^2 + 5 * alpha)
  14
  15/-- The closed-form ILG growth factor D(a, k) in EdS background (first-order in C). -/
  16noncomputable def growth_eds_ilg (P : KernelParams) (k a : ℝ) : ℝ :=
  17  a * (1 + (growth_prefactor P.alpha P.C) * (a / (k * P.tau0)) ^ P.alpha)
  18
  19/-- Growth rate f = d ln D / d ln a for the ILG growth factor. -/
  20noncomputable def f_growth_eds_ilg (P : KernelParams) (k a : ℝ) : ℝ :=
  21  let Xinv := a / (k * P.tau0)
  22  let B := growth_prefactor P.alpha P.C
  23  (1 + B * (1 + P.alpha) * Xinv ^ P.alpha) / (1 + B * Xinv ^ P.alpha)
  24
  25/-- The ILG-modified growth ODE in EdS background (Target B).
  26    Using ln(a) as the independent variable:
  27    D'' + (1/2) D' - (3/2) w(a,k) D = 0 -/
  28def GrowthODE_ILG (P : KernelParams) (k : ℝ) (D_func : ℝ → ℝ) : Prop :=
  29  ∀ a, 0 < a →
  30    let w := kernel P k a
  31    -- Expressed in terms of derivatives w.r.t a:
  32    -- a² D'' + (3/2) a D' - (3/2) w D = 0
  33    a^2 * (deriv (deriv D_func) a) + (3/2 : ℝ) * a * (deriv D_func a) - (3/2 : ℝ) * w * D_func a = 0
  34
  35/-- Theorem: The closed-form growth factor satisfies the ILG-modified growth ODE
  36    to first order in C (neglecting O(C²) terms). -/
  37theorem growth_satisfies_ode (P : KernelParams) (k : ℝ) (hk : 0 < k) :
  38    let B := growth_prefactor P.alpha P.C
  39    let D := fun a => a * (1 + B * (a / (k * P.tau0)) ^ P.alpha)
  40    ∀ a, 0 < a →
  41      (0.01 : ℝ) ≤ (a / (k * P.tau0)) →
  42      let w := kernel P k a
  43      let Xinv := (a / (k * P.tau0))
  44      let error_term := (3/2 : ℝ) * P.C * B * Xinv ^ (2 * P.alpha) * a
  45      a^2 * (deriv (deriv D) a) + (3/2 : ℝ) * a * (deriv D a) - (3/2 : ℝ) * w * D a + error_term = 0 := by
  46  intro B D a ha hXinv_large
  47  unfold growth_prefactor kernel
  48  set C := P.C
  49  set α := P.alpha
  50  set τ₀ := P.tau0
  51  set Xinv := a / (k * τ₀)
  52  -- D(a) = a + B * (k*τ₀)^(-α) * a^(1+α)
  53  have hD : D = fun a => a + B * (k * τ₀) ^ (-α) * a ^ (1 + α) := by
  54    funext a'; simp [D]
  55    rw [div_rpow (le_of_lt ha) (mul_nonneg (le_of_lt hk) (le_of_lt P.tau0_pos))]
  56    rw [Real.rpow_neg (mul_pos hk P.tau0_pos)]
  57    ring
  58  -- Compute derivatives
  59  have h_deriv_D : deriv D a = 1 + B * (1 + α) * Xinv ^ α := by
  60    rw [hD]
  61    rw [deriv_add differentiableAt_id']
  62    · simp
  63      rw [deriv_mul_const]
  64      · rw [deriv_rpow_const (1 + α)]
  65        · field_simp [Xinv]
  66          ring
  67        · exact Or.inl ha.ne'
  68      · exact differentiableAt_rpow_const (1 + α) (Or.inl ha.ne')
  69    · apply DifferentiableAt.mul_const
  70      exact differentiableAt_rpow_const (1 + α) (Or.inl ha.ne')
  71
  72  have h_deriv_2_D : deriv (deriv D) a = B * α * (1 + α) * Xinv ^ α / a := by
  73    -- D(a) = a + B * (k*τ₀)^(-α) * a^(1+α)
  74    -- deriv D = (fun a' => 1 + B * (1 + α) * (k*τ₀)^(-α) * a'^α)
  75    have h_deriv_eq : ∀ᶠ a' in 𝓝 a, deriv D a' = 1 + B * (1 + α) * (k * τ₀) ^ (-α) * a' ^ α := by
  76      filter_upwards [self_mem_nhds ha]
  77      intro a' ha'
  78      rw [hD, deriv_add differentiableAt_id']
  79      · simp
  80        rw [deriv_mul_const]
  81        · rw [deriv_rpow_const (1 + α)]
  82          · field_simp
  83            ring
  84          · exact Or.inl ha'.ne'
  85        · exact differentiableAt_rpow_const (1 + α) (Or.inl ha'.ne')
  86      · apply DifferentiableAt.mul_const
  87        exact differentiableAt_rpow_const (1 + α) (Or.inl ha'.ne')
  88
  89    rw [deriv_congr_ev h_deriv_eq]
  90    rw [deriv_add (differentiableAt_const 1)]
  91    · simp
  92      rw [deriv_mul_const]
  93      · rw [deriv_rpow_const α]
  94        · field_simp [Xinv]
  95          ring
  96        · exact Or.inl ha.ne'
  97      · exact differentiableAt_rpow_const α (Or.inl ha.ne')
  98    · apply DifferentiableAt.mul_const
  99      exact differentiableAt_rpow_const α (Or.inl ha.ne')
 100
 101  -- Plug in and simplify
 102
 103  -- Plug in and simplify
 104  simp only [h_deriv_D, h_deriv_2_D]
 105  unfold kernel
 106  have hmax : max 0.01 Xinv = Xinv := max_eq_right hXinv_large
 107  rw [hmax]
 108  field_simp [ha.ne']
 109  ring_nf
 110  simp [error_term]
 111  rw [mul_assoc, ← mul_add]
 112  convert mul_zero (a * Xinv ^ α)
 113  field_simp
 114  ring
 115
 116/-- Theorem: The ILG growth rate f(a,k) reduces to 1 in the GR limit (C=0). -/
 117theorem f_growth_gr_limit (P : KernelParams) (hC : P.C = 0) (k a : ℝ) (ha : 0 < a) :
 118    f_growth_eds_ilg P k a = 1 := by
 119  simp [f_growth_eds_ilg, growth_prefactor, hC]
 120
 121/-- Proof of the X-reciprocity identity for the growth factor D(a, k) (Target C). -/
 122theorem growth_x_reciprocity (P : KernelParams) (k a : ℝ) (ha : 0 < a) (hk : 0 < k) :
 123    let D := growth_eds_ilg P k
 124    let Q := fun a' k' => growth_eds_ilg P k' a' / a'
 125    a * (deriv (fun a' => Q a' k) a) = - k * (deriv (fun k' => Q a k') k) := by
 126  -- Q(a, k) = 1 + B * (a / (k * tau0)) ^ alpha
 127  -- Let Q_tilde(X) = 1 + B * (1/X)^alpha where X = k*tau0/a
 128  set B := growth_prefactor P.alpha P.C
 129  let Q_tilde := fun x => 1 + B * (1 / x) ^ P.alpha
 130  have h_eq : ∀ a' k', 0 < a' → 0 < k' → (growth_eds_ilg P k' a' / a') = Q_tilde (X_var k' a' P.tau0) := by
 131    intro a' k' ha' hk'
 132    simp [growth_eds_ilg, Q_tilde, X_var]
 133    field_simp [ha', hk', P.tau0_pos.ne']
 134  -- Application of the reciprocity identity from Reciprocity.lean
 135  have h_diff : DifferentiableAt ℝ Q_tilde (X_var k a P.tau0) := by
 136    apply DifferentiableAt.const_add
 137    apply DifferentiableAt.mul_const
 138    apply DifferentiableAt.rpow
 139    · apply DifferentiableAt.const_div
 140      · exact differentiableAt_id'
 141      · exact (X_var k a P.tau0_pos).ne' -- non-zero
 142    · exact differentiableAt_const _
 143    · apply Or.inl; apply div_pos; apply mul_pos hk P.tau0_pos; exact ha
 144  exact x_reciprocity_identity P.tau0 Q_tilde a k ha.ne' hk.ne' h_diff
 145
 146end ILG
 147end IndisputableMonolith
 148