rar_log_slope
plain-language theorem explainer
The definition supplies the logarithmic slope of the radial acceleration relation as 1 minus half the dynamical-time exponent α. Galaxy dynamics modelers cite it when converting the ILG weight scaling into the observed power-law index of the RAR. It is realized as a direct algebraic definition with no additional steps.
Claim. The logarithmic slope of the radial acceleration relation is given by $1 - α/2$, where α is the dynamical-time exponent appearing in the ILG weight function $w(r) ∝ (a_0 / a_{baryon})^{α/2}$.
background
The module treats the radial acceleration relation as a direct consequence of the ILG weight function. Observed acceleration satisfies $a_{obs}(r) = w(r) · a_{baryon}(r)$ with $w(r) ∝ (a_0 / a_{baryon})^{α/2}$, which rearranges at once to the power-law form $a_{obs} = C · a_0^{α/2} · a_{baryon}^{1 - α/2}$. Taking logarithms isolates the slope $d(log a_{obs})/d(log a_{baryon}) = 1 - α/2$ in log-log space.
proof idea
The definition is a one-line algebraic reduction that subtracts half the input exponent from unity, matching the power-law index stated in the module's RAR emergence statement.
why it matters
The definition isolates the explicit exponent required by the RAR Emergence theorem in Gravity.RAREmergence. It supports the module claim that the observed relation follows from the ILG weight under RS parameter locks, recovering the deep-MOND limit of slope 0.5 as α approaches 1. The construction sits downstream of the J-cost and phi-ladder structures that fix α.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.