Tdyn
plain-language theorem explainer
Tdyn supplies the orbital dynamical time T_dyn = 2 π r / v for circular motion at speed v and radius r. Gravity modelers in the Recognition Science framework cite it when converting between acceleration-parameterized and time-parameterized expressions for weight. The definition is a direct one-line algebraic formula with no additional lemmas required.
Claim. $T_ {dyn}(v, r) = 2 π r / v$, the orbital period for circular motion.
background
The module Gravity.ParameterizationBridge formalizes algebraic identities linking circular-orbit acceleration a = v²/r to dynamical time T_dyn = 2π r / v and the characteristic time T_0 = 2π √(r_0 / a_0). This provides the exact bridge between acceleration-based and time-based weight forms in the ILG gravity model. Upstream results include definitions of scale factors from phi powers in Cosmology.LargeScaleStructureFromRS and anchor radii r0 from Masses.Anchor, which feed into the parameterization. The local setting is the exact algebraic identities without sorrys, as stated in the module documentation.
proof idea
This is a definition, implemented as a direct algebraic expression 2 * Real.pi * r / v. No lemmas are applied; it is the standard formula for the period of circular motion.
why it matters
Tdyn feeds into the time-kernel definitions w_t and related lemmas in Gravity.ILG, enabling the time-parameterized weight forms. It fills the parameterization bridge step in the gravity module, connecting to the broader Recognition Science framework where dynamical times relate to the phi-ladder and forcing chain. No open questions are touched here as it is fully defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.