def definition def or abbrev

`PsiPotential`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  36noncomputable def PsiPotential (g : Metric) (ψ : RefreshField) (C_lag : ℝ) : ℝ :=

proof body

Definition body.

  37  Fields.potential_action ψ (C_lag ^ 2) g default_volume
  38
  39/-- ψ-sector action placeholder parameterised by (C_lag, α): kinetic + potential. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

gr_limit_reduces in IndisputableMonolith.Relativity.ILG.Action decl_use
gr_limit_zero in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiAction in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiActionP in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (5)

Lean names referenced from this declaration's body.

C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
potential_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
default_volume in IndisputableMonolith.Relativity.ILG.Action decl_use
Metric in IndisputableMonolith.Relativity.ILG.Action decl_use
RefreshField in IndisputableMonolith.Relativity.ILG.Action decl_use