`S`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.ILG.Action
domain: Relativity
line: 133 · 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 133.

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

used by

formal source

 130  S_total inp.fst inp.snd p
 131
 132/-- Full ILG action: S[g, ψ; C_lag, α] := S_EH[g] + S_ψ[g,ψ]. -/
 133noncomputable def S (g : Metric) (ψ : RefreshField) (C_lag α : ℝ) : ℝ :=
 134  S_EH g + PsiAction g ψ C_lag α
 135
 136/-- GR-limit reduction: when C_lag = 0 and α = 0, the ψ-sector vanishes. -/
 137theorem gr_limit_reduces (g : Metric) (ψ : RefreshField) :
 138  S g ψ 0 0 = S_EH g := by
 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). -/
 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.