  38    _ = 0.006 := by norm_num
  39    _ < 0.01 := by norm_num
  40
  41class GWObservationalFacts : Prop where
  42  gw170817_bound : |c_T_squared_RS - 1| < 1e-15
  43
  44theorem GW170817_bound_satisfied [GWObservationalFacts] :
  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.