a_obs_ilg
plain-language theorem explainer
a_obs_ilg defines the observed acceleration in the ILG model as the product of the weight function w_accel and the baryonic acceleration. Galaxy dynamicists deriving the radial acceleration relation from causal-response models cite this when converting the weight scaling into an explicit power law. The definition is realized as a direct one-line product that enables algebraic reduction in the RAR emergence theorems.
Claim. The observed acceleration satisfies $a_{obs} = w(a_{baryon}) · a_{baryon}$, where $w$ is the ILG weight function of the characteristic acceleration $a_0$, the baryonic acceleration $a_{baryon}$, and the dynamical exponent $α$.
background
The Radial Acceleration Relation Emergence module shows that the empirical RAR arises as a direct algebraic consequence of the ILG weight function. In this setting the observed acceleration is written $a_{obs}(r) = w(r) · a_{baryon}(r)$, with the weight scaling as $w ∝ (a_0 / a_{baryon})^{α/2}$ and $α$ the dynamical-time exponent locked by Recognition Science forcing. The module imports the definition of $α$ from Constants.Alpha, the structure of J-cost from PhiForcingDerived, and ledger factorization from DAlembert.LedgerFactorization.
proof idea
This is a one-line definition that multiplies the result of w_accel by a_baryon. Downstream identities are obtained by unfolding the definition and applying rpow identities to collect the exponents $α/2$ and $1 - α/2$.
why it matters
The definition supplies the core expression for $a_{obs}$ that is algebraically rewritten in rar_power_law to produce the exact RAR power law $a_{obs} = a_0^{α/2} · a_{baryon}^{1 - α/2}$. It anchors the RAR Emergence Theorem and the universality statement in rar_is_universal, showing how the observed relation follows from the ILG weight without galaxy-specific assumptions. In the Recognition Science framework it links the phi-ladder and eight-tick octave to galactic dynamics via the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.