time_ratio_sq_eq_accel_ratio_mul_r_ratio
plain-language theorem explainer
The declaration proves the exact kinematic relation (T_dyn / T_0)^2 = (a_0 / a) * (r / r_0) for circular orbits defined by a = v^2/r and T_dyn = 2π r / v. Modelers comparing acceleration-based and time-based parameterizations in gravitational dynamics would reference this identity as the core bridge. The proof is a direct algebraic reduction that invokes the squared forms of the dynamical time and reference time expressions, then normalizes via field_simp.
Claim. For positive real numbers $v, r, a_0, r_0$, let $a = v^2 / r$, $T = 2π r / v$, and $T_0 = 2π √(r_0 / a_0)$. Then $(T / T_0)^2 = (a_0 / a) * (r / r_0)$.
background
In the Gravity.ParameterizationBridge module, the acceleration for circular motion is defined as $a = v^2 / r$, the dynamical time as $T_{dyn} = 2π r / v$, and the reference time as $T_0 = 2π √(r_0 / a_0)$. These definitions establish the precise algebraic link between acceleration-parameterized and time-parameterized forms of orbital relations. The module states that all bridge identities are fully proven without sorry. This theorem relies on the upstream lemmas accel_mul_Tdyn_sq, which encodes $a · T_{dyn}^2 = 4 π^2 r$, and T0_sq, which gives the squared reference time.
proof idea
The proof performs direct algebraic verification. It first confirms non-zero conditions for the quantities involved. It rewrites the left-hand side using the square of a quotient, then substitutes the squared expressions from accel_mul_Tdyn_sq and T0_sq. Finally, it applies field_simp to clear denominators and normalize the equation.
why it matters
This identity serves as the foundational bridge in the parameterization module, directly feeding the rearranged form accel_ratio_eq_time_ratio_sq_mul_r0_over_r and the exponent mapping accel_power_eq_time_power_at_r_eq_r0. It fills the kinematic core of the acceleration-to-time mapping in Recognition Science gravity models, consistent with the phi-forcing and ledger structures upstream. No open questions are indicated for this proved statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.