w_accel
The ILG weight function supplies the scaling w(a) = (a₀ / a)^{α/2} that converts baryonic acceleration to observed acceleration in galactic dynamics models. Researchers deriving the radial acceleration relation cite this parameterization as the input to the power-law emergence theorems. The definition is a direct algebraic expression encoding the square-root exponent from the acceleration-time bridge in the Recognition Science framework.
claimThe ILG weight function is defined by $w(a_0, a, α) = (a_0 / a)^{α/2}$, where $a_0$ is the characteristic acceleration scale, $a$ is the baryonic acceleration, and $α$ is the dynamical-time exponent.
background
The module derives the radial acceleration relation as a consequence of the ILG weight function in the Recognition Science model of gravity. The observed acceleration satisfies $a_{obs} = w(a_{baryon}) · a_{baryon}$, with the weight scaling as a power law in the ratio of accelerations. The upstream result from PrimitiveDistinction establishes the foundational axioms leading to the structural conditions used in this gravity module.
proof idea
This declaration is a direct definition with no additional lemmas or tactics applied. It encodes the ILG scaling as the real power $(a_0 / a)$ raised to $(α / 2)$.
why it matters in Recognition Science
This definition provides the core scaling relation for the RAR Emergence Theorem proved in rar_power_law, which establishes $a_{obs} = a_0^{α/2} · a_{baryon}^{1 - α/2}$. It implements the ILG prediction step outlined in the module documentation, connecting to the Recognition Science treatment of the radial acceleration relation with exponent $1 - α/2$. The downstream theorems a_obs_ilg and rar_power_law_emergence rely on it to derive the exact power-law form from the weight function.
scope and limits
- Does not specify numerical values for a0 or α.
- Does not include a multiplicative constant C in the weight function.
- Does not prove any emergence theorem for the RAR.
- Does not reference the phi-ladder or other Recognition Science constants.
Lean usage
def a_obs_ilg (a₀ a_baryon α : ℝ) : ℝ := w_accel a₀ a_baryon α * a_baryonformal statement (Lean)
61def w_accel (a₀ a α : ℝ) : ℝ := (a₀ / a) ^ (α / 2)
proof body
Definition body.
62
63/-- The observed (effective) acceleration from ILG.
64 \(a_{\rm obs} = w(a_{\rm baryon}) \cdot a_{\rm baryon}\) -/