ilg_alpha

formal source

  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
  81  T_dyn : ℝ           -- Rotation period
  82  τ0 : ℝ              -- Recognition tick
  83  α : ℝ               -- ILG exponent
  84  C_lag : ℝ           -- Coupling constant
  85  w_predicted : ℝ     -- Predicted weight
  86  h_w : w_predicted = 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1)
  87
  88/-- Construct a lab-scale prediction for a given device. -/
  89def mkLabPrediction (T_dyn τ0 α C_lag : ℝ) : LabScalePrediction where
  90  T_dyn := T_dyn
  91  τ0 := τ0
  92  α := α
  93  C_lag := C_lag
  94  w_predicted := 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1)
  95  h_w := rfl
  96
  97/-! ## Connection to 8-Tick Schedule -/
  98
  99/-- The 8-tick window discipline divides the rotation into 8 phases.