PsiKinetic

formal source

  28
  29/-- ψ-sector kinetic term: (α/2) ∫ √(-g) g^{μν} (∂_μ ψ)(∂_ν ψ) d^4x.
  30    Now uses actual Fields.kinetic_action. -/
  31noncomputable def PsiKinetic (g : Metric) (ψ : RefreshField) (α : ℝ) : ℝ :=
  32  α * Fields.kinetic_action ψ g default_volume
  33
  34/-- ψ-sector mass/potential term: (C_lag/2) ∫ √(-g) ψ² d^4x.
  35    Now uses actual Fields.potential_action. -/
  36noncomputable def PsiPotential (g : Metric) (ψ : RefreshField) (C_lag : ℝ) : ℝ :=
  37  Fields.potential_action ψ (C_lag ^ 2) g default_volume
  38
  39/-- ψ-sector action placeholder parameterised by (C_lag, α): kinetic + potential. -/
  40noncomputable def PsiAction (g : Metric) (ψ : RefreshField) (C_lag α : ℝ) : ℝ :=
  41  PsiKinetic g ψ α + PsiPotential g ψ C_lag
  42
  43/-- Global parameter bundle for ILG (α, C_lag). -/
  44structure ILGParams where
  45  alpha : ℝ
  46  cLag  : ℝ
  47  deriving Inhabited
  48
  49/-- Index conventions (symbolic): use natural numbers as abstract tensor indices. -/
  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