def
definition
S_EH
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 23.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
jcost_stationarity_implies_regge -
eh_proportional_to_R -
jacobi_variation_structural -
error_vanishes -
regge_to_eh_convergence_axiom -
deficit_neg_of_angle_excess -
metric_matrix_invertible_at -
ReggeConvergenceHypothesis -
gr_limit_cov -
gr_limit_on -
gr_limit_reduces -
gr_limit_zero -
L_cov -
S -
S_on -
S_total -
S_total_cov -
VolumeElement -
CheegerMullerWitness -
cheeger_muller_witness_trivial -
regge_to_eh_convergence_discharged -
regge_to_eh_convergence_proof
formal source
20 Geometry.ricci_scalar g x₀ -- Scaffold: use single-point value
21
22/-- Alias for consistency. -/
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