w_accel

formal source

  58    - \(a_0\): characteristic acceleration scale
  59    - \(\alpha\): dynamical-time exponent (RS: alphaLock ≈ 0.191)
  60    - The factor 1/2 comes from the acceleration↔time bridge -/
  61def w_accel (a₀ a α : ℝ) : ℝ := (a₀ / a) ^ (α / 2)
  62
  63/-- The observed (effective) acceleration from ILG.
  64    \(a_{\rm obs} = w(a_{\rm baryon}) \cdot a_{\rm baryon}\) -/
  65def a_obs_ilg (a₀ a_baryon α : ℝ) : ℝ :=
  66  w_accel a₀ a_baryon α * a_baryon
  67
  68/-! ## RAR Emergence Theorem -/
  69
  70/-- **RAR Emergence Theorem (exact form):**
  71    The observed acceleration is a power-law function of baryonic acceleration:
  72
  73    \(a_{\rm obs} = a_0^{\alpha/2} \cdot a_{\rm baryon}^{1 - \alpha/2}\)
  74
  75    This is the RAR with exponent \(1 - \alpha/2\).
  76-/
  77theorem rar_power_law (a₀ a_baryon α : ℝ) (ha0 : 0 < a₀) (ha : 0 < a_baryon) :
  78    a_obs_ilg a₀ a_baryon α = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) := by
  79  unfold a_obs_ilg w_accel
  80  -- (a₀/a)^(α/2) * a = a₀^(α/2) * a^(-α/2) * a = a₀^(α/2) * a^(1 - α/2)
  81  -- This is straightforward algebra using rpow identities
  82  have ha0' : 0 ≤ a₀ := le_of_lt ha0
  83  have ha' : 0 ≤ a_baryon := le_of_lt ha
  84  -- Split the ratio power: (a₀/a)^(α/2) = a₀^(α/2) / a^(α/2)
  85  rw [Real.div_rpow ha0' ha' (α / 2)]
  86  -- Convert a / a^(α/2) into a^(1-α/2)
  87  have hsub : a_baryon ^ (1 - α / 2) = a_baryon ^ (1 : ℝ) / a_baryon ^ (α / 2) := by
  88    simpa using (Real.rpow_sub ha (1 : ℝ) (α / 2))
  89  -- Finish by reassociation.
  90  calc
  91    (a₀ ^ (α / 2) / a_baryon ^ (α / 2)) * a_baryon