`rs_lab_prediction_value`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Flight.GravityBridge on GitHub at line 181.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 203end
 204
 205end GravityBridge
 206end Flight
 207end IndisputableMonolith

papers checked against this theorem

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