Gravity Raremergence Rar Log Slope

The log-log slope

The Radial Acceleration Relation (RAR) is an empirical rule in galaxy dynamics: for any galaxy, the observed acceleration a_obs is a tight function of the acceleration predicted from its visible baryonic matter a_baryon. On a log-log plot, this relation is nearly a straight line with a slope near 0.8. The Recognition Science framework derives this slope from a simple power-law model, rather than fitting it to data.

In the framework, the observed acceleration is modeled as the baryonic acceleration multiplied by a weight function: a_obs = w(a_baryon) · a_baryon. The weight function is defined as w(a) = C · (a₀/a)^(α/2), where a₀ is a characteristic acceleration scale and α is a dynamical-time exponent. This choice models the idea that the response of a galaxy's dynamics depends on the local acceleration ratio.

From this definition, the framework proves a theorem: the observed acceleration is exactly a_obs = a₀^(α/2) · a_baryon^(1 - α/2). This is a power law with exponent 1 - α/2. The declaration rar_log_slope (a discrete record of the slope value in the framework's machine-checked library) simply names this exponent as the log-log slope: slope = 1 - α/2. For the framework's locked value of α ≈ 0.191, this gives a slope of about 0.8055.

This is a mathematical consequence of the model, not a new empirical claim. The slope is derived from the power-law form; it does not by itself explain why galaxies follow this relation. The framework also notes that if α were 1, the slope would be 0.5, matching the deep-MOND limit, but the framework's own value is different.

In Recognition Science, this result is one step in a larger program: it shows how a universal galaxy scaling law can emerge from a simple, forced cost structure. The declaration does not claim to fit the RAR scatter, to explain the physical mechanism behind the weight function, or to prove that the RAR holds for all galaxies. It establishes a clean mathematical relationship between the model's exponent and the observed slope.

/-- **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]

/-- **RAR slope (log-log):**
    In log-log space, the RAR has slope \(d(\log a_{\rm obs})/d(\log a_{\rm baryon}) = 1 - \alpha/2\).

    For \(\alpha = 0.389\): slope ≈ 0.8055
    For MOND-like (\(\alpha \to 1\)): slope → 0.5 (deep MOND)
-/
def rar_log_slope (α : ℝ) : ℝ := 1 - α / 2

theorem rar_slope_rs_value : rar_slope_rs = 1 - (1 - 1/phi) / 4 := by
  unfold rar_slope_rs alphaLock
  ring

What this page does not claim

The RAR is an empirical law with intrinsic scatter, not a theorem of the framework. The framework does not explain the physical origin of the weight function w(a). The slope value 0.8055 is a derived consequence of the model, not a measured constant.

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: