accel
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not incorporate relativistic corrections or spacetime curvature.
- Does not restrict v or r to positive values or impose non-zero conditions.
- Does not extend to non-circular or time-varying orbits.
- Does not assign units or numerical scales to v and r.
Lean usage
example (v r : ℝ) : accel v r = v ^ 2 / r := by rflformal statement (Lean)
29def accel (v r : ℝ) : ℝ := v^2 / r
proof body
Definition body.
30
31/-- Orbital (dynamical) time for circular motion (one full revolution). -/