kron

formal source

  50abbrev Index : Type := Nat
  51
  52/-- Kronecker delta δᵤᵥ (symbolic). -/
  53@[simp] noncomputable def kron (μ ν : Index) : ℝ := if μ = ν then 1 else 0
  54
  55/-- Raise/lower index placeholders (identity maps in the scaffold). -/
  56@[simp] def raiseIndex (μ : Index) : Index := μ
  57@[simp] def lowerIndex (μ : Index) : Index := μ
  58
  59/-- Variation notation scaffolding: delta of a scalar expression (symbolic identity). -/
  60@[simp] noncomputable def deltaVar (x : ℝ) : ℝ := x
  61
  62/-- Functional derivative: δS/δx for action functional S and state variable x. -/
  63noncomputable def dS_dx (S_func : ℝ → ℝ) (x₀ : ℝ) : ℝ :=
  64  deriv S_func x₀
  65
  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