`optionA_testable`

definition

show as: view math explainer →

module: IndisputableMonolith.Flight.GravityBridge
domain: Flight
line: 187 · 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 187.

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

rsLabPrediction IndisputableMonolith.Flight.GravityBridge

formal source

 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.