rotationPeriod

formal source

  47/-! ## Device Dynamical Timescale -/
  48
  49/-- A rotating device with angular velocity ω has period T = 2π/ω. -/
  50def rotationPeriod (ω : ℝ) (hω : ω ≠ 0) : ℝ := 2 * Real.pi / ω
  51
  52/-- The dynamical timescale of a φ-spiral rotor is its rotation period. -/
  53def deviceDynamicalTime (ω : ℝ) (hω : ω ≠ 0) : ℝ := rotationPeriod ω hω
  54
  55/-! ## ILG Weight at Lab Scales -/
  56
  57/-- Reference recognition tick τ₀ in seconds (from RS constants).
  58    τ₀ = 1/(8 ln φ) in natural units ≈ 7.3 × 10⁻¹⁵ s. -/
  59def tau0_seconds : ℝ := 7.3e-15
  60
  61/-- A typical lab rotation period (e.g., 1000 RPM = 0.06 s). -/
  62def typicalLabPeriod_seconds : ℝ := 0.06
  63
  64/-- Ratio T_dyn/τ₀ for typical lab device. This is enormous (~10¹³). -/
  65def labScaleRatio : ℝ := typicalLabPeriod_seconds / tau0_seconds
  66
  67/-- The ILG exponent α = (1 - φ⁻¹)/2 ≈ 0.191.
  68    Using the RS constant φ = (1 + √5)/2. -/
  69def ilg_alpha : ℝ := (1 - 1/phi) / 2
  70
  71/-- Lab-scale weight deviation: for α ≈ 0.191 and ratio ≈ 10¹³,
  72    the term (T_dyn/τ₀)^α ≈ (10¹³)^0.191 ≈ 10^2.5 ≈ 316.
  73
  74    However, C_lag is typically 10⁻³ to 10⁻⁵ for consistency with
  75    solar system tests. So the deviation is:
  76      w - 1 = C_lag * 315 ≈ 0.3 (at C_lag = 10⁻³)
  77
  78    This is a TESTABLE prediction if C_lag is not too small.
  79-/
  80structure LabScalePrediction where