accel_mul_Tdyn_sq
plain-language theorem explainer
The core kinematic identity states that acceleration times the square of dynamical time equals four pi squared times radius for nonzero velocity and radius. Researchers bridging acceleration and time parameterizations in Recognition Science gravity models cite this result. The proof is a direct term-mode reduction that unfolds the definitions then applies field simplification followed by ring.
Claim. For nonzero real numbers $v$ and $r$, let $a = v^2/r$ be the centripetal acceleration and $T = 2$ $pi$ $r/v$ the orbital period. Then $a$ $T^2 = 4$ $pi^2$ $r$.
background
The module formalizes exact algebraic identities relating circular-orbit acceleration $a = v^2/r$, orbital dynamical time $T = 2$ $pi$ $r/v$, and the reference characteristic time $T_0 = 2$ $pi$ $sqrt(r_0/a_0)$. These identities form the precise bridge between acceleration-parameterized and time-parameterized weight forms. The dynamical time definition is $T(v,r) := 2$ $pi$ $r/v$. Upstream structures supply discrete phi-tiers and J-cost calibration but are not invoked in this purely kinematic step.
proof idea
The proof unfolds the definitions of acceleration and dynamical time, applies field_simp under the nonzero assumptions on $v$ and $r$ to clear denominators, and finishes with the ring tactic on the resulting expression.
why it matters
This supplies the base identity used by the downstream theorem time_ratio_sq_eq_accel_ratio_mul_r_ratio, which equates the squared time ratio to the product of inverse acceleration ratio and radius ratio. It completes the parameterization bridge in the Gravity module and anchors the relation to the characteristic time $T_0$ from SyncMinimization. In the Recognition framework the result supports the kinematic relations underlying the eight-tick octave and dimensional forcing from T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.