beta_growth

formal source

  38
  39    where α = alphaLock = (1-1/φ)/2 ≈ 0.191.
  40    The prefactor φ^(-3/2) ≈ 0.486 comes from the CPM paper's C = φ^(-3/2). -/
  41noncomputable def beta_growth (k tau0 : ℝ) : ℝ :=
  42  (2 / 3) * phi ^ (-(3/2 : ℝ)) * (k * tau0) ^ (-alphaLock)
  43
  44/-- β is positive for positive k and τ₀. -/
  45theorem beta_growth_pos (k tau0 : ℝ) (hk : 0 < k) (ht : 0 < tau0) :
  46    0 < beta_growth k tau0 := by
  47  unfold beta_growth
  48  apply mul_pos
  49  · apply mul_pos (by norm_num : (0:ℝ) < 2/3)
  50    exact Real.rpow_pos_of_pos phi_pos _
  51  · exact Real.rpow_pos_of_pos (mul_pos hk ht) _
  52
  53/-! ## The Growth Factor D(a,k) -/
  54
  55/-- The ILG-modified linear growth factor.
  56    D(a,k) = a * (1 + β(k) * a^α)^(1/(1+α))
  57
  58    In GR (β = 0): D = a (matter-dominated growth).
  59    Under ILG: D > a (enhanced growth from the ILG kernel). -/
  60noncomputable def D_growth (a k tau0 : ℝ) : ℝ :=
  61  a * (1 + beta_growth k tau0 * a ^ alphaLock) ^ (1 / (1 + alphaLock))
  62
  63/-- D is positive for positive a. -/
  64theorem D_growth_pos (a k tau0 : ℝ) (ha : 0 < a) (hk : 0 < k) (ht : 0 < tau0) :
  65    0 < D_growth a k tau0 := by
  66  unfold D_growth
  67  apply mul_pos ha
  68  apply Real.rpow_pos_of_pos
  69  have hbeta := beta_growth_pos k tau0 hk ht
  70  have ha_pow : 0 < a ^ alphaLock := Real.rpow_pos_of_pos ha _
  71  linarith [mul_pos hbeta ha_pow]