C_lag_RS

formal source

 160
 161/-- The RS prediction: C_lag is derived from φ, not a free parameter.
 162    Specifically, C_lag = φ⁻⁵ ≈ 0.0902 in the time-kernel formula. -/
 163def C_lag_RS : ℝ := Real.rpow phi (-5)
 164
 165/-- With C_lag = φ⁻⁵ and typical lab scales, the predicted deviation is:
 166    w - 1 = φ⁻⁵ * ((0.06 / 7.3e-15)^0.191 - 1)
 167          ≈ 0.09 * 315
 168          ≈ 28
 169
 170    This would be a LARGE effect if true! The null hypothesis would fail.
 171-/
 172def rsLabPrediction : LabScalePrediction :=
 173  mkLabPrediction typicalLabPeriod_seconds tau0_seconds ilg_alpha C_lag_RS
 174
 175/-- The RS prediction yields w ≈ 29, not w ≈ 1.
 176    This is either:
 177    (a) A falsifiable prediction (test it!)
 178    (b) Evidence that C_lag is suppressed at lab scales
 179    (c) Evidence that T_dyn ≠ T_rot for a non-gravitationally-bound system
 180-/
 181def rs_lab_prediction_value : Prop :=
 182  25 < rsLabPrediction.w_predicted ∧ rsLabPrediction.w_predicted < 35
 183
 184/-! ## Interpretation Options -/
 185
 186/-- Option A: ILG applies at lab scales → large deviation → testable. -/
 187def optionA_testable : Prop :=
 188  rsLabPrediction.w_predicted > 10
 189
 190/-- Option B: ILG only applies to gravitationally-bound systems.
 191    For a rotating device, T_dyn = ∞ (not bound), so w = 1. -/
 192def optionB_bound_only : Prop :=
 193  ∀ (device : LabScalePrediction), ¬(device.T_dyn > 0 ∧ device.T_dyn < 1e10) →