T0_sq
plain-language theorem explainer
T0_sq proves that the square of the characteristic dynamical time equals 4 pi squared times the ratio of the reference length to the reference acceleration. Researchers deriving exact kinematic bridges between acceleration and orbital period in circular motion would cite this identity. The proof unfolds the T0 definition, confirms non-negativity of the ratio, invokes the square-root squaring identity, and finishes with ring simplification.
Claim. For real numbers $r_0$ with $r_0 = 0$ or $r_0 > 0$ and $a_0 > 0$, let $T_0 = 2$ $pi$ $sqrt(r_0 / a_0)$. Then $T_0^2 = 4 pi^2 (r_0 / a_0)$.
background
The module Gravity.ParameterizationBridge supplies the exact algebraic relations that convert between acceleration-parameterized and dynamical-time-parameterized descriptions of circular orbits. The characteristic time is introduced by the sibling definition T0 as $T_0 = 2 pi sqrt(r_0 / a_0)$. The module states that every identity in the acceleration-time bridge is fully proven with no sorrys. Upstream material includes the basic real-number arithmetic lemmas used to manipulate squares and square roots.
proof idea
The tactic proof first unfolds the definition of T0. It then records that the ratio r0/a0 is nonnegative and applies the lemma that the square of the square root recovers the original nonnegative argument. The remainder is a direct algebraic expansion: the square distributes over the product, the square-root term cancels, and ring normalizes the resulting expression.
why it matters
T0_sq supplies the squared form required by the immediate downstream theorem time_ratio_sq_eq_accel_ratio_mul_r_ratio, which states the exact bridge identity $(T_dyn / T_0)^2 = (a_0 / a)(r / r_0)$. The result therefore anchors the kinematic foundation of the entire parameterization bridge inside the gravity module. It directly supports the conversion between acceleration and time forms that the module presents as the precise link underlying weight relations in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.