`gr_limit_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.ILG.Action
domain: Relativity
line: 143 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.ILG.Action on GitHub at line 143.

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

 140  simp [Fields.kinetic_action, Fields.potential_action]
 141
 142/-- GR-limit for bundled parameters (α=0, C_lag=0). -/
 143theorem gr_limit_zero (g : Metric) (ψ : RefreshField) :
 144  S_total g ψ { alpha := 0, cLag := 0 } = S_EH g := by
 145  unfold S_total PsiAction PsiKinetic PsiPotential
 146  simp [Fields.kinetic_action, Fields.potential_action]
 147
 148/-- GR-limit for bundled inputs. -/
 149theorem gr_limit_on (inp : ActionInputs) :
 150  S_on inp { alpha := 0, cLag := 0 } = S_EH inp.fst := by
 151  unfold S_on S_total
 152  exact gr_limit_reduces inp.fst inp.snd
 153
 154end ILG
 155end Relativity
 156end IndisputableMonolith

papers checked against this theorem

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