`optionB_bound_only`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Flight.GravityBridge on GitHub at line 192.

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

 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.