Gravity Raremergence Rar Is Universal

The universal relation

The Radial Acceleration Relation, or RAR, is an empirical pattern in galaxy data. For any galaxy, astronomers can estimate the acceleration that should come from its visible matter, the baryonic acceleration a_baryon. They can also measure the actual observed acceleration a_obs, which is larger. The RAR states that a_obs is a smooth function of a_baryon alone, with only about 0.1 dex of scatter, across galaxies that differ wildly in mass, size, and shape.

In Recognition Science, the framework models this relation with a specific formula. The observed acceleration equals the baryonic acceleration multiplied by a weight w(a) = C * (a0/a)^(alpha/2), where a0 is a characteristic acceleration scale and alpha is a dynamical-time exponent. The theorem rar_power_law proves that this definition is equivalent to a clean power law: a_obs = a0^(alpha/2) * a_baryon^(1 - alpha/2). With alpha = 0.389, the exponent is about 0.8.

The declaration rar_is_universal captures the key consequence. It proves that if a0 and alpha are global constants shared by all galaxies, then the ratio of observed accelerations between any two galaxies equals the ratio of their baryonic accelerations raised to the same power (1 - alpha/2). In plain language: the same function f describes every galaxy, regardless of its individual properties. The universality is not assumed; it follows from the shared constants and the local form of the weight function.

This result does not claim that the RAR is exact for every real galaxy. The framework's own note lists sources of scatter: observational errors, variations in a morphology factor, and deviations from steady-state circular orbits. It also does not derive the value of alpha from first principles; the value alphaLock ≈ 0.191 appears as a parameter lock, and the slope 1 - alpha/2 is a derived quantity, not a measured one.

/-- **RAR Emergence Theorem (exact form):**
    The observed acceleration is a power-law function of baryonic acceleration:

    \(a_{\rm obs} = a_0^{\alpha/2} \cdot a_{\rm baryon}^{1 - \alpha/2}\)

    This is the RAR with exponent \(1 - \alpha/2\).
-/
theorem rar_power_law (a₀ a_baryon α : ℝ) (ha0 : 0 < a₀) (ha : 0 < a_baryon) :
    a_obs_ilg a₀ a_baryon α = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) := by
  unfold a_obs_ilg w_accel
  -- (a₀/a)^(α/2) * a = a₀^(α/2) * a^(-α/2) * a = a₀^(α/2) * a^(1 - α/2)
  -- This is straightforward algebra using rpow identities
  have ha0' : 0 ≤ a₀ := le_of_lt ha0
  have ha' : 0 ≤ a_baryon := le_of_lt ha
  -- Split the ratio power: (a₀/a)^(α/2) = a₀^(α/2) / a^(α/2)
  rw [Real.div_rpow ha0' ha' (α / 2)]
  -- Convert a / a^(α/2) into a^(1-α/2)
  have hsub : a_baryon ^ (1 - α / 2) = a_baryon ^ (1 : ℝ) / a_baryon ^ (α / 2) := by
    simpa using (Real.rpow_sub ha (1 : ℝ) (α / 2))
  -- Finish by reassociation.
  calc
    (a₀ ^ (α / 2) / a_baryon ^ (α / 2)) * a_baryon
        = a₀ ^ (α / 2) * (a_baryon / a_baryon ^ (α / 2)) := by ring
    _ = a₀ ^ (α / 2) * (a_baryon ^ (1 : ℝ) / a_baryon ^ (α / 2)) := by
          simp [Real.rpow_one]
    _ = a₀ ^ (α / 2) * a_baryon ^ (1 - α / 2) := by
          -- rewrite the right factor using `hsub`
          simp [hsub]

/-- The RAR is universal (same function for all galaxies) when α and a₀ are global. -/
theorem rar_is_universal
    (a₀ α : ℝ) (ha0 : 0 < a₀)
    (galaxy1_a_baryon galaxy2_a_baryon : ℝ)
    (h1 : 0 < galaxy1_a_baryon) (h2 : 0 < galaxy2_a_baryon) :
    -- The ratio of observed accelerations equals the ratio of baryonic accelerations
    -- raised to the power (1 - α/2)
    a_obs_ilg a₀ galaxy1_a_baryon α / a_obs_ilg a₀ galaxy2_a_baryon α =
    (galaxy1_a_baryon / galaxy2_a_baryon) ^ (1 - α / 2) := by
  rw [rar_power_law a₀ galaxy1_a_baryon α ha0 h1]
  rw [rar_power_law a₀ galaxy2_a_baryon α ha0 h2]
  -- The a₀^(α/2) factors cancel, leaving (a1/a2)^(1-α/2)
  set p : ℝ := 1 - α / 2
  have ha0_ne : (a₀ ^ (α / 2)) ≠ 0 := by
    exact ne_of_gt (Real.rpow_pos_of_pos ha0 (α / 2))
  have hcancel :
      (a₀ ^ (α / 2) * galaxy1_a_baryon ^ p) / (a₀ ^ (α / 2) * galaxy2_a_baryon ^ p)
        = (galaxy1_a_baryon ^ p) / (galaxy2_a_baryon ^ p) := by
    simpa [mul_assoc, mul_left_comm, mul_comm] using
      (mul_div_mul_left (galaxy1_a_baryon ^ p) (galaxy2_a_baryon ^ p) ha0_ne)
  rw [hcancel]
  have h1' : 0 ≤ galaxy1_a_baryon := le_of_lt h1
  have h2' : 0 ≤ galaxy2_a_baryon := le_of_lt h2
  have hdiv : (galaxy1_a_baryon / galaxy2_a_baryon) ^ p =
      galaxy1_a_baryon ^ p / galaxy2_a_baryon ^ p := by
    simpa [p] using (Real.div_rpow h1' h2' p)
  -- Rewrite the RHS using `hdiv`.
  simp [hdiv]

What this page does not claim

The framework does not claim that the RAR holds exactly for every galaxy; it allows for scatter from observational errors and morphology variations. The framework does not derive the numerical value of the exponent alpha from first principles; it appears as a parameter lock. The framework does not claim that the RAR is a unique prediction; the same functional form could arise from other models.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/RAREmergence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: