gr_limit_reduces

formal source

 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