def
definition
S_on
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.ILG.Action on GitHub at line 129.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
126abbrev ActionInputs := Metric × RefreshField
127
128/-- Apply total action on bundled inputs. -/
129noncomputable def S_on (inp : ActionInputs) (p : ILGParams) : ℝ :=
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