def
definition
default_volume
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 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
23noncomputable def S_EH := EHAction
24
25/-- Default volume element for action integrals. -/
26noncomputable def default_volume : VolumeElement :=
27 { grid_spacing := 1.0, grid_spacing_pos := by norm_num }
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 := μ