`gr_limit_on`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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.