time_power_eq_accel_power_at_r_eq_r0
plain-language theorem explainer
The theorem equates the α-power of the dynamical time ratio to the (α/2)-power of the inverse acceleration ratio at the reference radius r0. Modelers switching between time-based and acceleration-based parameterizations in Recognition Science gravity frameworks would invoke this identity. The proof proceeds by invoking the dual acceleration-to-time bridge with exponent α/2 and simplifying the resulting exponent via algebraic cancellation.
Claim. At the characteristic radius $r = r_0$, let $a = v^2 / r_0$, $T = 2π r_0 / v$, and $T_0 = 2π √(r_0 / a_0)$. Then for positive real numbers $v, r_0, a_0, α$, $(T / T_0)^α = (a_0 / a)^{α/2}$.
background
The module ParameterizationBridge establishes algebraic relations between circular orbit acceleration $a = v^2 / r$, dynamical period $T_{dyn} = 2π r / v$, and reference time $T_0 = 2π √(r_0 / a_0)$. These identities allow exact conversion between acceleration-parameterized and time-parameterized forms of gravitational models. The upstream result accel_power_eq_time_power_at_r_eq_r0 states the dual relation $(a_0 / a)^α = (T / T_0)^{2α}$ at r = r0. The current theorem is its time-to-acceleration counterpart.
proof idea
The proof applies the already-proved theorem accel_power_eq_time_power_at_r_eq_r0 with the halved exponent α/2. It then uses the ring tactic to confirm that twice the halved exponent recovers α, and concludes by symmetry of the equality.
why it matters
This theorem completes the bidirectional exponent bridge in the Gravity.ParameterizationBridge module, enabling seamless translation between time-exponent and acceleration-exponent forms at the reference scale. It supports the broader Recognition Science effort to derive gravitational dynamics from the unified forcing chain and the Recognition Composition Law. No immediate downstream uses are recorded, but it closes the parameterization symmetry for models involving arbitrary exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.