`c_T_squared_derived`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.GW.PropagationSpeed
domain: Relativity
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.GW.PropagationSpeed on GitHub at line 48.

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

formal source

  45  |c_T_squared_RS - 1| < 1e-15 :=
  46  GWObservationalFacts.gw170817_bound
  47
  48theorem c_T_squared_derived :
  49  c_T_squared 0 0 = 1 ∧
  50  (∀ α C_lag, ∃ coeff, c_T_squared α C_lag = 1 + coeff * (α * C_lag)) := by
  51  constructor
  52  · exact c_T_squared_GR_limit
  53  · intro α C_lag
  54    refine ⟨0.01, ?_⟩
  55    simp [c_T_squared]
  56
  57end GW
  58end Relativity
  59end IndisputableMonolith

papers checked against this theorem

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