w_accel
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.