theorem proved term proof

`c_T_squared_derived`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  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

proof body

Term-mode proof.

  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

depends on (4)

Lean names referenced from this declaration's body.

C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
coeff in IndisputableMonolith.Pipelines decl_use
c_T_squared in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use
c_T_squared_GR_limit in IndisputableMonolith.Relativity.GW.PropagationSpeed decl_use