`L_density`

definition

show as: view math explainer →

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

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

  66
  67/-- Symbolic ILG Lagrangian density (toy): L = (∂ψ)^2/2 − m^2 ψ^2/2 + cLag·alpha.
  68    Here we treat all terms as scalars to keep the scaffold compiling. -/
  69noncomputable def L_density (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ :=
  70  (p.alpha ^ 2) / 2 - (p.cLag ^ 2) / 2 + p.cLag * p.alpha
  71
  72/-- Covariant scalar Lagrangian pieces (symbolic). -/
  73noncomputable def L_kin (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := (p.alpha ^ 2) / 2
  74noncomputable def L_mass (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := (p.cLag ^ 2) / 2
  75/-- Potential Lagrangian - depends on metric and refresh field configuration.
  76    Placeholder using coupling constant scaled by field variance. -/
  77noncomputable def L_pot (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := p.cLag / 2
  78noncomputable def L_coupling (_g : Metric) (_ψ : RefreshField) (p : ILGParams) : ℝ := p.cLag * p.alpha
  79
  80/-- Covariant scalar Lagrangian (toy): L_cov = L_kin − L_mass + L_pot + L_coupling. -/
  81noncomputable def L_cov (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
  82  L_kin g ψ p - L_mass g ψ p + L_pot g ψ p + L_coupling g ψ p
  83
  84/-- Covariant total action using L_cov: S_cov = S_EH + ∫ L_cov (toy: scalar sum). -/
  85noncomputable def S_total_cov (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
  86  S_EH g + L_cov g ψ p
  87
  88/-- GR-limit for S_total_cov (α=0, C_lag=0). -/
  89theorem gr_limit_cov (g : Metric) (ψ : RefreshField) :
  90  S_total_cov g ψ { alpha := 0, cLag := 0 } = S_EH g := by
  91  unfold S_total_cov L_cov L_kin L_mass L_pot L_coupling
  92  simp
  93
  94/-- Convenience total action using bundled params. -/
  95noncomputable def S_total (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=
  96  S_EH g + PsiAction g ψ p.cLag p.alpha
  97
  98/-- ψ-sector action using bundled parameters. -/
  99noncomputable def PsiActionP (g : Metric) (ψ : RefreshField) (p : ILGParams) : ℝ :=

papers checked against this theorem

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