a_obs_flat
plain-language theorem explainer
The definition supplies the observed centripetal acceleration a_obs = v_f^2 / r for flat galactic rotation curves. Galaxy dynamics researchers deriving the baryonic Tully-Fisher relation from ILG modifications would cite this when linking asymptotic velocity to baryonic mass via the RAR scaling. It is implemented as a direct one-line definition of the centripetal formula.
Claim. The observed centripetal acceleration at radius $r$ for a flat rotation curve with velocity $v_f$ is $a_0 = v_f^2 / r$.
background
The BTFREmergence module records the algebraic setup relating ILG/RAR scaling to BTFR-style power laws. For flat rotation curves at large $r$, centripetal acceleration is $a = v_f^2 / r$ while baryonic acceleration is $GM_b / r^2$. The RAR power-law form from RAREmergence supplies $a_obs = a_0^{α/2} · a_baryon^{1 - α/2}$, which rearranges to the BTFR slope $β = 4 / (1 + α/2)$ ≈ 3.35 for $α ≈ 0.389$.
proof idea
This is a direct definition implementing the centripetal acceleration formula for flat rotation curves. No lemmas are applied; it is a one-line algebraic abbreviation.
why it matters
This definition is used in the BTFR emergence theorem btfr_mass_velocity_relation, which states that for an ILG-modified galaxy with flat rotation curve, $M_b ∝ v_f^β$ where $β$ depends on the modification regime. It fills the algebraic setup for deriving the BTFR slope from the RAR form, connecting to the ILG framework. The module notes that a fully structural BTFR with nontrivial constant independent of $M_b$ remains in progress.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.