Gravity Raremergence

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

THEOREM rar_is_universal · IndisputableMonolith/Gravity/RAREmergence.lean

MODEL a_obs_ilg · IndisputableMonolith/Gravity/RAREmergence.lean

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: