def
definition
PsiPotential
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.ILG.Action on GitHub at line 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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