IndisputableMonolith.Gravity.RAREmergence

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Radial Acceleration Relation (RAR) Emergence from ILG
   6
   7This module proves that the Radial Acceleration Relation (RAR) emerges
   8as a mathematical consequence of the ILG weight function.
   9
  10## The RAR
  11
  12The empirical RAR states that observed acceleration \(a_{\rm obs}\) correlates
  13tightly with baryonic acceleration \(a_{\rm baryon}\) across all galaxies:
  14
  15  \(a_{\rm obs} = f(a_{\rm baryon})\)
  16
  17with intrinsic scatter ≈ 0.1 dex.
  18
  19## ILG Prediction
  20
  21The ILG/causal-response model has:
  22
  23  \(a_{\rm obs}(r) = w(r) \cdot a_{\rm baryon}(r)\)
  24
  25where the weight function scales as:
  26
  27  \(w(r) \propto (a_0 / a_{\rm baryon})^{\alpha/2}\)
  28
  29The acceleration-space exponent is \(\alpha/2\) where \(\alpha\) is the
  30dynamical-time exponent. Under RS parameter locks, \(\alpha = \text{alphaLock} \approx 0.191\).
  31
  32## Main Result
  33
  34**Theorem (RAR Emergence):**
  35Given the ILG weight \(w = C \cdot (a_0/a)^{\alpha/2}\), the RAR takes the form:
  36
  37  \(a_{\rm obs} = C \cdot a_0^{\alpha/2} \cdot a_{\rm baryon}^{1 - \alpha/2}\)
  38
  39This is a power-law RAR with exponent \(1 - \alpha/2 \approx 0.8\) for \(\alpha = 0.389\).
  40
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Gravity
  45namespace RAREmergence
  46
  47open Real
  48open Constants
  49
  50noncomputable section
  51
  52/-! ## ILG Weight Function -/
  53
  54/-- The ILG weight function (acceleration parameterization).
  55    \(w(a) = C \cdot (a_0/a)^{\alpha/2}\) for baryonic acceleration \(a\).
  56
  57    Parameters:
  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
  92        = a₀ ^ (α / 2) * (a_baryon / a_baryon ^ (α / 2)) := by ring
  93    _ = a₀ ^ (α / 2) * (a_baryon ^ (1 : ℝ) / a_baryon ^ (α / 2)) := by
  94          simp [Real.rpow_one]
  95    _ = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) := by
  96          -- rewrite the right factor using `hsub`
  97          simp [hsub]
  98
  99/-- Same result as `rar_power_law`, but stated directly as an algebraic identity
 100    in the "weight times baryonic acceleration" form. -/
 101theorem rar_power_law_emergence
 102    (a₀ a_baryon α : ℝ) (ha0 : 0 < a₀) (ha : 0 < a_baryon) :
 103    (a₀ / a_baryon) ^ (α / 2) * a_baryon = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) := by
 104  simpa [a_obs_ilg, w_accel] using (rar_power_law a₀ a_baryon α ha0 ha)
 105
 106/-- Alias for the main RAR emergence statement, kept for stable downstream references. -/
 107theorem rar_emergence_direct
 108    (a₀ a_baryon α : ℝ) (ha0 : 0 < a₀) (ha : 0 < a_baryon) :
 109    a_obs_ilg a₀ a_baryon α = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) :=
 110  rar_power_law a₀ a_baryon α ha0 ha
 111
 112/-- **RAR slope (log-log):**
 113    In log-log space, the RAR has slope \(d(\log a_{\rm obs})/d(\log a_{\rm baryon}) = 1 - \alpha/2\).
 114
 115    For \(\alpha = 0.389\): slope ≈ 0.8055
 116    For MOND-like (\(\alpha \to 1\)): slope → 0.5 (deep MOND)
 117-/
 118def rar_log_slope (α : ℝ) : ℝ := 1 - α / 2
 119
 120/-- The RS-derived value of the RAR slope.
 121    Using \(\alpha_{\rm RS} = (1 - 1/\varphi)/2\) as the acceleration exponent:
 122
 123    slope = 1 - α_RS/2 = 1 - (1 - 1/φ)/4
 124-/
 125def rar_slope_rs : ℝ := 1 - alphaLock / 2
 126
 127theorem rar_slope_rs_value : rar_slope_rs = 1 - (1 - 1/phi) / 4 := by
 128  unfold rar_slope_rs alphaLock
 129  ring
 130
 131/-- RAR slope for a specific α value (for numerical comparison).
 132    Example: α = 0.389 → slope = 1 - 0.389/2 ≈ 0.8055
 133-/
 134def rar_slope_at (α : ℝ) : ℝ := 1 - α / 2
 135
 136/-! ## Universality of the RAR
 137
 138The key feature of the RAR is its **universality**: the same function \(f\)
 139works for all galaxies despite their different masses, sizes, and morphologies.
 140
 141In the ILG model, universality follows from:
 1421. The weight function \(w(a)\) depends only on the local acceleration ratio \(a_0/a\)
 1432. The parameters \((a_0, \alpha)\) are global constants shared by all galaxies
 1443. The morphology factor \(\xi(f_{\rm gas})\) provides only modest modulation
 145
 146**Note**: The scatter in the RAR (≈ 0.1 dex empirically) arises from:
 147- Observational errors
 148- Variations in \(\xi\) with morphology
 149- Deviations from steady-state circular orbits
 150-/
 151
 152/-- The RAR is universal (same function for all galaxies) when α and a₀ are global. -/
 153theorem rar_is_universal
 154    (a₀ α : ℝ) (ha0 : 0 < a₀)
 155    (galaxy1_a_baryon galaxy2_a_baryon : ℝ)
 156    (h1 : 0 < galaxy1_a_baryon) (h2 : 0 < galaxy2_a_baryon) :
 157    -- The ratio of observed accelerations equals the ratio of baryonic accelerations
 158    -- raised to the power (1 - α/2)
 159    a_obs_ilg a₀ galaxy1_a_baryon α / a_obs_ilg a₀ galaxy2_a_baryon α =
 160    (galaxy1_a_baryon / galaxy2_a_baryon) ^ (1 - α / 2) := by
 161  rw [rar_power_law a₀ galaxy1_a_baryon α ha0 h1]
 162  rw [rar_power_law a₀ galaxy2_a_baryon α ha0 h2]
 163  -- The a₀^(α/2) factors cancel, leaving (a1/a2)^(1-α/2)
 164  set p : ℝ := 1 - α / 2
 165  have ha0_ne : (a₀ ^ (α / 2)) ≠ 0 := by
 166    exact ne_of_gt (Real.rpow_pos_of_pos ha0 (α / 2))
 167  have hcancel :
 168      (a₀ ^ (α / 2) * galaxy1_a_baryon ^ p) / (a₀ ^ (α / 2) * galaxy2_a_baryon ^ p)
 169        = (galaxy1_a_baryon ^ p) / (galaxy2_a_baryon ^ p) := by
 170    simpa [mul_assoc, mul_left_comm, mul_comm] using
 171      (mul_div_mul_left (galaxy1_a_baryon ^ p) (galaxy2_a_baryon ^ p) ha0_ne)
 172  rw [hcancel]
 173  have h1' : 0 ≤ galaxy1_a_baryon := le_of_lt h1
 174  have h2' : 0 ≤ galaxy2_a_baryon := le_of_lt h2
 175  have hdiv : (galaxy1_a_baryon / galaxy2_a_baryon) ^ p =
 176      galaxy1_a_baryon ^ p / galaxy2_a_baryon ^ p := by
 177    simpa [p] using (Real.div_rpow h1' h2' p)
 178  -- Rewrite the RHS using `hdiv`.
 179  simp [hdiv]
 180
 181end
 182
 183end RAREmergence
 184end Gravity
 185end IndisputableMonolith
 186