IndisputableMonolith.Gravity.ILGGrowthFactor

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# ILG Growth Factor (Dark-Energy + Hubble-Tension Papers)
   6
   7Formalizes the ILG-modified growth factor D(a,k) and growth rate f(a,k)
   8from the Dark-Energy and Hubble-Tension papers.
   9
  10## Core Definitions
  11
  12- D(a,k) = a * (1 + β(k) * a^α)^(1/(1+α))
  13- β(k) = (2/3) * φ^(-3/2) * (k*τ₀)^(-α)
  14- f(a,k) = 1 + [α/(1+α)] * β*a^α / (1 + β*a^α)
  15
  16where α = alphaLock ≈ 0.191 and τ₀ is the fundamental tick.
  17
  18## Key Properties
  19
  20- D(a,k) → a as β → 0 (GR limit)
  21- D(a,k) > a for β > 0 (ILG enhances growth)
  22- f(a,k) → 1 as β → 0 (GR limit: f = 1 in matter domination)
  23- f(a,k) > 1 for β > 0 (ILG enhances growth rate)
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Gravity
  28namespace ILGGrowthFactor
  29
  30open Constants
  31
  32noncomputable section
  33
  34/-! ## The β(k) Function -/
  35
  36/-- The ILG growth kernel parameter β(k).
  37    β(k) = (2/3) * φ^(-3/2) * (k*τ₀)^(-α)
  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]
  72
  73/-- In the GR limit (β → 0), D(a) = a * 1 = a. -/
  74theorem D_growth_gr_limit (a : ℝ) (ha : 0 < a) :
  75    a * (1 + 0 * a ^ alphaLock) ^ (1 / (1 + alphaLock)) = a := by
  76  simp [zero_mul, Real.one_rpow]
  77
  78/-- D ≥ a always (ILG enhances or preserves growth). -/
  79theorem D_growth_ge_a (a k tau0 : ℝ) (ha : 0 < a) (hk : 0 < k) (ht : 0 < tau0) :
  80    a ≤ D_growth a k tau0 := by
  81  unfold D_growth
  82  have hbeta := beta_growth_pos k tau0 hk ht
  83  have ha_pow : 0 < a ^ alphaLock := Real.rpow_pos_of_pos ha _
  84  have h_inner : 1 ≤ 1 + beta_growth k tau0 * a ^ alphaLock := by
  85    linarith [mul_pos hbeta ha_pow]
  86  have h_exp : 0 < 1 / (1 + alphaLock) := by
  87    apply div_pos one_pos
  88    linarith [alphaLock_pos]
  89  calc a = a * 1 := by ring
  90    _ ≤ a * (1 + beta_growth k tau0 * a ^ alphaLock) ^ (1 / (1 + alphaLock)) := by
  91        apply mul_le_mul_of_nonneg_left _ (le_of_lt ha)
  92        exact Real.one_le_rpow h_inner h_exp.le
  93
  94/-! ## The Growth Rate f(a,k) -/
  95
  96/-- The ILG-modified growth rate.
  97    f(a,k) = d ln D / d ln a
  98           = 1 + [α/(1+α)] * β*a^α / (1 + β*a^α)
  99
 100    In GR (β = 0): f = 1 (matter domination).
 101    Under ILG: f > 1 (enhanced growth rate). -/
 102noncomputable def f_growth (a k tau0 : ℝ) : ℝ :=
 103  let beta := beta_growth k tau0
 104  let ba := beta * a ^ alphaLock
 105  1 + (alphaLock / (1 + alphaLock)) * ba / (1 + ba)
 106
 107/-- f > 1 for positive β and a (ILG enhances growth rate). -/
 108theorem f_growth_gt_one (a k tau0 : ℝ) (ha : 0 < a) (hk : 0 < k) (ht : 0 < tau0) :
 109    1 < f_growth a k tau0 := by
 110  unfold f_growth
 111  simp only
 112  have hbeta := beta_growth_pos k tau0 hk ht
 113  have ha_pow : 0 < a ^ alphaLock := Real.rpow_pos_of_pos ha _
 114  have hba : 0 < beta_growth k tau0 * a ^ alphaLock := mul_pos hbeta ha_pow
 115  have h1ba : 0 < 1 + beta_growth k tau0 * a ^ alphaLock := by linarith
 116  have h_frac : 0 < alphaLock / (1 + alphaLock) := by
 117    exact div_pos alphaLock_pos (by linarith [alphaLock_pos])
 118  have h_ratio : 0 < beta_growth k tau0 * a ^ alphaLock /
 119      (1 + beta_growth k tau0 * a ^ alphaLock) :=
 120    div_pos hba h1ba
 121  linarith [mul_pos h_frac h_ratio]
 122
 123/-- In the GR limit: f → 1. -/
 124theorem f_growth_gr_limit : f_growth 1 1 0 = 1 := by
 125  unfold f_growth beta_growth
 126  simp [mul_zero, Real.rpow_zero, zero_mul]
 127
 128/-! ## Certificate -/
 129
 130structure GrowthFactorCert where
 131  D_positive : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → 0 < D_growth a k tau0
 132  D_ge_a : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → a ≤ D_growth a k tau0
 133  f_gt_one : ∀ a k tau0 : ℝ, 0 < a → 0 < k → 0 < tau0 → 1 < f_growth a k tau0
 134  beta_positive : ∀ k tau0 : ℝ, 0 < k → 0 < tau0 → 0 < beta_growth k tau0
 135
 136theorem growth_factor_cert : GrowthFactorCert where
 137  D_positive := D_growth_pos
 138  D_ge_a := D_growth_ge_a
 139  f_gt_one := f_growth_gt_one
 140  beta_positive := beta_growth_pos
 141
 142end
 143
 144end ILGGrowthFactor
 145end Gravity
 146end IndisputableMonolith
 147