Pith. sign in
module module moderate

IndisputableMonolith.Gravity.RAREmergence

show as:
view Lean formalization →

Module deriving the Radial Acceleration Relation (RAR) from the ILG weight in Recognition Science gravity. It defines w(a)=C(a0/a)^{α/2} on baryonic acceleration and shows the observed acceleration obeys a power-law RAR whose log-slope is fixed by the RS dynamical-time exponent α≈0.191 and is universal. Galaxy-dynamics and MOND researchers would cite the emergence and slope results. Argument is mostly definitional plus direct algebraic slope computations.

claimThe module introduces the ILG weight $w(a)=C\cdot(a_0/a)^{\alpha/2}$ on baryonic acceleration $a$, the ILG observed acceleration, and the Radial Acceleration Relation as an emergent power law. It records the logarithmic slope, the RS-specialized slope at the locked $\alpha\approx0.191$, pointwise slope evaluation, and universality of the RAR slope.

background

In Recognition Science gravity, Information-Limited Gravity (ILG) replaces dark-matter halos by an acceleration-dependent weight on the baryonic field. The weight is the power law $w(a)=C\cdot(a_0/a)^{\alpha/2}$, where $a_0$ is a characteristic acceleration scale and $\alpha$ is the dynamical-time exponent (RS lock $\alpha\approx0.191$). The factor $1/2$ comes from the acceleration–time bridge.

The Radial Acceleration Relation (RAR) is the empirical link between observed centripetal acceleration and Newtonian baryonic acceleration in disk galaxies. This module formalizes how that relation, its log-slope, and its universality follow from the ILG weight.

The sole external import is Constants, which supplies the fundamental RS time quantum $\tau_0=1$ tick and RS-native units.

proof idea

Definition-and-identity module rather than a deep proof development. It introduces the ILG weight and the observed ILG acceleration, then derives the RAR power-law form both directly and via an emergence lemma. Logarithmic slopes are obtained by differentiation/algebraic rewrite; the RS slope is the same expression with the locked $\alpha$ substituted; a pointwise slope map and a universality statement close the chain. Steps are equational, not tactic-heavy.

why it matters in Recognition Science

RAR emergence is a central phenomenological claim of RS gravity: the same $\alpha$ fixed elsewhere in the framework should reproduce the galaxy-scale acceleration relation without dark matter. The module supplies the Lean definitions and elementary slope derivations that any later comparison to rotation-curve or SPARC-style data would cite.

No downstream dependents are recorded in the graph yet; the natural consumers are the sibling results on power-law emergence, RS slope value, and universality, which form the interface between ILG and observational RAR tests. It sits in the Gravity domain beside the RS-native constants for $c$, $\hbar$, and $G$.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)