accel
plain-language theorem explainer
The definition supplies the centripetal acceleration a = v²/r for circular orbits as the base kinematic relation in the parameterization bridge. Gravity modelers cite it when converting between acceleration-based and time-based weight kernels or exponent mappings. Its body is a direct one-line abbreviation of the standard Newtonian expression with no auxiliary lemmas.
Claim. The centripetal acceleration for circular motion with orbital speed $v$ and radius $r$ is given by $a = v^2 / r$.
background
The module formalizes exact algebraic identities relating circular-orbit acceleration, dynamical time $T_{dyn} = 2π r / v$, and the reference time $T_0 = 2π √(r_0 / a_0)$. These identities bridge acceleration-parameterized and time-parameterized forms of gravitational weight. Upstream results supply the unit element in LogicInt, LogicRat, Spin, and PhiClosed structures to support the surrounding arithmetic operations.
proof idea
The definition is a direct one-line abbreviation of the Newtonian centripetal acceleration formula. No lemmas or tactics are invoked; the expression v^2 / r is taken as primitive for all downstream identities.
why it matters
This definition is the kinematic foundation for the five bridge theorems in the module, including accel_mul_Tdyn_sq (a T_dyn² = 4 π² r) and the exponent bridges accel_power_eq_time_power_at_r_eq_r0 and time_power_eq_accel_power_at_r_eq_r0. It supplies the precise translation between acceleration exponents and time exponents at the characteristic radius, enabling the acceleration-time duality required by the Recognition Science gravity parameterization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.