Encyclopedia Gravity Gravity Raremergence
ARTICLE 3 claims 2 theorems 1 model
Gravity Raremergence
Gravity raremergence is the name for the way observed galactic acceleration follows from baryonic acceleration through a single weight function, a relation the module proves as a theorem.
Raremergence as a derived law
Gravity raremergence is the process by which the observed acceleration in a galaxy is not a new force but a re-expression of the baryonic acceleration through a universal weight function. The module establishes this as a theorem: given the weight function w_accel, which depends only on the ratio of a characteristic acceleration scale to the local baryonic acceleration, the observed acceleration is a power law of the baryonic acceleration. The theorem rar_power_law proves this identity exactly for positive acceleration scales.
The weight function is defined as w(a) = (a₀/a)^(α/2), where a₀ is a characteristic acceleration scale and α is the dynamical-time exponent. The observed acceleration is then a_obs = w(a_baryon) · a_baryon. The theorem shows this equals a₀^(α/2) · a_baryon^(1 − α/2), a power-law relation with exponent 1 − α/2. For the RS parameter lock α ≈ 0.191, the slope in log-log space is about 0.9, though the module notes a slope near 0.8 for α = 0.389.
The module also proves universality: the same function applies to all galaxies when α and a₀ are global constants. The theorem rar_is_universal shows that the ratio of observed accelerations between two galaxies equals the ratio of their baryonic accelerations raised to the same power. This universality is what makes the empirical Radial Acceleration Relation a single curve rather than a family of galaxy-specific relations.
What the module does not do is derive the values of α and a₀ from first principles. The parameter α is locked to a value from the RS framework, and a₀ remains a scale. The theorems are algebraic identities conditional on those parameters. The empirical match to the observed RAR is a separate check, not part of the proof.
THEOREM rar_power_law · IndisputableMonolith/Gravity/RAREmergence.lean
/-- **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]
THEOREM rar_is_universal · IndisputableMonolith/Gravity/RAREmergence.lean
/-- 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]
MODEL a_obs_ilg · IndisputableMonolith/Gravity/RAREmergence.lean
/-- The observed (effective) acceleration from ILG.
\(a_{\rm obs} = w(a_{\rm baryon}) \cdot a_{\rm baryon}\) -/
def a_obs_ilg (a₀ a_baryon α : ℝ) : ℝ :=
w_accel a₀ a_baryon α * a_baryon
What this page does not claim
This answer does not claim that the values of α and a₀ are derived from first principles. This answer does not claim that the empirical RAR is reproduced by the theorem without additional parameter input. This answer does not claim that gravity raremergence explains all galactic dynamics beyond the algebraic power-law relation.
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:
- How is the characteristic acceleration scale a₀ determined within the RS framework?
- What empirical data sets are used to test the predicted RAR slope against the measured relation?
- How does the dynamical-time exponent α relate to the golden ratio φ in the RS parameter locks?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
- THEOREMThe theorem rar_power_law proves this identity exactly for positive acceleration scales. rar_power_law · IndisputableMonolith/Gravity/RAREmergence.lean
- THEOREMThe theorem rar_is_universal shows that the ratio of observed accelerations between two galaxies equals the ratio of their baryonic accelerations raised to the same power. rar_is_universal · IndisputableMonolith/Gravity/RAREmergence.lean
- MODELThe observed acceleration is then a_obs = w(a_baryon) · a_baryon. a_obs_ilg · IndisputableMonolith/Gravity/RAREmergence.lean