theorem proved term proof

`gr_limit_reduces`

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

formal statement (Lean)

 137theorem gr_limit_reduces (g : Metric) (ψ : RefreshField) :
 138  S g ψ 0 0 = S_EH g := by

proof body

Term-mode proof.

 139  unfold S PsiAction PsiKinetic PsiPotential
 140  simp [Fields.kinetic_action, Fields.potential_action]
 141
 142/-- GR-limit for bundled parameters (α=0, C_lag=0). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

gr_limit_on in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (11)

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
kinetic_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
potential_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
Metric in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiAction in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiKinetic in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiPotential in IndisputableMonolith.Relativity.ILG.Action decl_use
RefreshField in IndisputableMonolith.Relativity.ILG.Action decl_use
S in IndisputableMonolith.Relativity.ILG.Action decl_use
S_EH in IndisputableMonolith.Relativity.ILG.Action decl_use