theorem proved term proof

`gr_limit_cov`

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

formal statement (Lean)

  89theorem gr_limit_cov (g : Metric) (ψ : RefreshField) :
  90  S_total_cov g ψ { alpha := 0, cLag := 0 } = S_EH g := by

Term-mode proof.

  91  unfold S_total_cov L_cov L_kin L_mass L_pot L_coupling
  92  simp
  93
  94/-- Convenience total action using bundled params. -/

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
L_coupling in IndisputableMonolith.Relativity.ILG.Action decl_use
L_cov in IndisputableMonolith.Relativity.ILG.Action decl_use
L_kin in IndisputableMonolith.Relativity.ILG.Action decl_use
L_mass in IndisputableMonolith.Relativity.ILG.Action decl_use
L_pot in IndisputableMonolith.Relativity.ILG.Action decl_use
Metric in IndisputableMonolith.Relativity.ILG.Action decl_use
RefreshField in IndisputableMonolith.Relativity.ILG.Action decl_use
S_EH in IndisputableMonolith.Relativity.ILG.Action decl_use
S_total_cov in IndisputableMonolith.Relativity.ILG.Action decl_use