rotationPeriod
plain-language theorem explainer
A rotating device with angular velocity ω has rotation period T = 2π/ω. Researchers modeling lab-scale ILG weight predictions in the Flight domain cite this when supplying the dynamical timescale to the weight kernel w_t(T_dyn, τ₀). The definition is a direct algebraic formula with no lemmas or tactics required.
Claim. For angular velocity $ω ≠ 0$, the rotation period is $T = 2π / ω$.
background
The Flight.GravityBridge module connects the ILG weight kernel to the Flight/Propulsion model. It formalizes T_dyn for rotating lab devices as the rotation period, with τ₀ ≈ 7.3 fs as the recognition tick and α = (1 - φ^{-1})/2 as the lag exponent. Upstream structures from PhiForcingDerived supply the J-cost framework while NucleosynthesisTiers provide φ-tier densities for scaling.
proof idea
The definition is a one-line algebraic expression that directly implements the standard period formula under the hypothesis ω ≠ 0.
why it matters
This definition is invoked by deviceDynamicalTime to set the dynamical timescale for ILG weight calculations at lab scales where T_rot ≫ τ₀ implies w ≈ 1. It addresses the module's first key question on T_dyn for rotating lab devices and supports the null-result prediction. It ties into the eight-tick octave and phi-ladder landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.