recognition / Flight / Flight.GravityBridge / RunningCoupling

structure

`RunningCoupling`

definition

show as: view math explainer →

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

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.

depends on

used by

RunningCoupling IndisputableMonolith.Physics.RGTransport

formal source

 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.