btfr_slope_deep
plain-language theorem explainer
BTFR slope in the flat rotation limit is defined as 4. Galaxy dynamics researchers modeling ILG-modified rotation curves cite this constant when establishing the strong mass-velocity relation M_b = v_f^4 / (G a_0). The assignment records the exact exponent that follows from the asymptotic flat-curve constraint together with the deep-regime RAR scaling.
Claim. In the deep ILG regime the BTFR exponent satisfies $β = 4$.
background
The module records the algebraic link between ILG/RAR scaling and the empirical BTFR M_b ∝ v_f^β. For flat rotation curves the centripetal acceleration is a = v_f^2 / r while the ILG rule gives a_obs = w(a_baryon) · a_baryon; at large radii a_baryon reduces to the Keplerian GM_b / r^2. The RAR power-law form a_obs = a_0^{α/2} a_baryon^{1-α/2} then yields the slope relation β = 4 / (1 + α/2). In the deep regime this forces β = 4 independently of baryonic mass.
proof idea
Direct definition that hard-codes the constant 4 derived from the flat-curve algebra.
why it matters
Supplies the exact deep-regime exponent required by BTFRCert to certify the universal proportionality constant 1/(G a_0) independent of M_b. It closes the deep-regime case in the ILG-to-BTFR derivation of the module. The downstream theorem btfr_deep_regime_exponent invokes it to state M_b = v_f^4 / (G a_0) with the constant independent of baryonic mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.