accel_power_eq_time_power_at_r_eq_r0
plain-language theorem explainer
This theorem establishes the exact algebraic relation (a0/a)^α = (T_dyn/T0)^{2α} at the reference radius r = r0 for positive reals v, r0, a0, α. Researchers rewriting orbital or gravitational models between acceleration kernels and dynamical-time kernels cite it to preserve exponent consistency under the parameterization bridge. The proof reduces the claim to the sibling time-ratio identity at equal radii, verifies positivity of the ratios, and applies real exponent multiplication rules.
Claim. For positive reals $v, r_0, a_0, α$, let $a = v^2/r_0$, $T = 2π r_0/v$, $T_0 = 2π √(r_0/a_0)$. Then $(a_0/a)^α = (T/T_0)^{2α}$.
background
The module formalizes algebraic identities relating circular-orbit acceleration $a = v^2/r$, dynamical time $T_{dyn} = 2π r/v$, and reference time $T_0 = 2π √(r_0/a_0)$. These identities supply the precise bridge between acceleration-parameterized and time-parameterized weight forms. The theorem specializes the general bridge to the case of equal radii r = r0. It depends on the upstream identity time_ratio_sq_eq_accel_ratio_mul_r_ratio, which equates the squared time ratio to the acceleration ratio scaled by the radius ratio.
proof idea
The tactic proof introduces the local definitions of a, T and Tref. It calls time_ratio_sq_eq_accel_ratio_mul_r_ratio at equal radii, simplifies the radius ratio to 1, and obtains (T/Tref)^2 = a0/a. Separate subgoals establish positivity of T, Tref and the ratio T/Tref. The main equality is recovered by rewriting the left side as ((T/Tref)^2)^α, applying Real.rpow_mul on the non-negative ratio, and using norm_cast to equate the exponents.
why it matters
This result supplies one direction of the exponent mapping inside the parameterization bridge module and is invoked directly by the sibling theorem time_power_eq_accel_power_at_r_eq_r0 that gives the inverse form with exponent α/2. It supports consistent rewriting of models between acceleration space and time space at the characteristic radius, consistent with the alpha definitions appearing in the Constants.Alpha module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.