`rsLabPrediction`

definition

show as: view math explainer →

module: IndisputableMonolith.Flight.GravityBridge
domain: Flight
line: 172 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Flight.GravityBridge on GitHub at line 172.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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) →
 194    device.w_predicted = 1
 195
 196/-- Option C: C_lag is scale-dependent (runs with energy/length).
 197    At lab scales, C_lag → 0, preserving w ≈ 1. -/
 198structure RunningCoupling where
 199  C_lag_of_scale : ℝ → ℝ  -- C_lag as function of length scale
 200  h_galactic : C_lag_of_scale 1e20 = C_lag_RS  -- Galactic scale
 201  h_lab : C_lag_of_scale 1 < 1e-10  -- Lab scale (1 meter)
 202

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.