deviceDynamicalTime
plain-language theorem explainer
The declaration defines the dynamical timescale of a rotating device as its rotation period 2π/ω for nonzero angular velocity ω. Researchers modeling ILG weight at laboratory scales cite this to identify T_dyn with the period of a φ-spiral rotor. It is a one-line wrapper around the rotationPeriod definition.
Claim. For a device rotating at angular velocity $ω ≠ 0$, the dynamical timescale $T_{dyn}(ω)$ equals the rotation period $2π/ω$.
background
The Flight.GravityBridge module connects the ILG weight kernel $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ to the Flight model, with $τ_0 ≈ 7.3$ fs the recognition tick and $α ≈ 0.191$. It addresses the dynamical timescale $T_{dyn}$ for a rotating lab device and the prediction that $w ≈ 1$ at lab scales where $T_{rot} ≫ τ_0$ by many orders of magnitude. The upstream rotationPeriod definition states that a rotating device with angular velocity ω has period $T = 2π/ω$. The tick is the fundamental RS time quantum, equal to 1 in RS-native units, and one octave equals eight ticks.
proof idea
This is a one-line wrapper that applies the rotationPeriod definition, substituting the expression $2 * Real.pi / ω$ under the given nonzero hypothesis.
why it matters
This definition supplies $T_{dyn}$ for the ILG weight kernel in the Flight module, supporting the null-result claim that laboratory rotating devices exhibit no measurable deviation from Newtonian weight. It directly addresses the module's key question on the dynamical timescale of a rotating lab device and ties the eight-tick octave to device rotation. No downstream uses are recorded yet, but it prepares the ground for explicit ILG weight calculations at lab scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.