falsifierTriggered

formal source

 153  predicted_thrust_from_ILG : ℝ
 154  discrepancy : ℝ := |measured_thrust - predicted_thrust_from_ILG|
 155
 156def falsifierTriggered (f : GravityFalsifier) (threshold : ℝ) : Prop :=
 157  f.discrepancy > threshold
 158
 159/-! ## RS-Specific Predictions -/
 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. -/