accel_ratio_eq_time_ratio_sq_mul_r0_over_r
plain-language theorem explainer
Algebraic rearrangement yields the relation between acceleration ratio and squared dynamical time ratio scaled by characteristic radius ratio in orbital systems. Parameterization studies in gravity models cite this when equating acceleration-based and time-based weight forms. Proof applies the companion squared-time identity then cancels radius factors via field simplification and congruence.
Claim. Let $a = v^2/r$, $T = 2π r/v$, and $T_0 = 2π √(r_0/a_0)$. For positive real numbers $v,r,a_0,r_0$, $a_0/a = (T/T_0)^2 · (r_0/r)$.
background
This module formalizes the exact algebraic identities that relate circular-orbit acceleration $a = v^2/r$, orbital/dynamical time $T_{dyn} = 2π r/v$, and the common characteristic time $T_0 = 2π √(r_0/a_0)$. These identities are the precise bridge underlying the relationship between acceleration-parameterized and time-parameterized weight forms. All bridge identities in the module are fully proven.
proof idea
The proof introduces local definitions for a, T, and Tref. It applies the sibling lemma time_ratio_sq_eq_accel_ratio_mul_r_ratio to obtain (T/Tref)^2 = (a0/a) · (r/r0). It then multiplies both sides by (r0/r), cancels the resulting (r/r0)·(r0/r)=1 using field_simp on the nonzero hypotheses, and concludes by symmetry of the resulting equality.
why it matters
This identity completes the basic bridge set in the ParameterizationBridge module, enabling consistent exponent mappings such as the acceleration exponent versus time exponent relation at the characteristic radius. It supports the framework's goal of exact algebraic relations between physical parameterizations without approximation. The module status records that all such bridge identities are fully proven.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.