No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
48noncomputable def potential_action
49 (φ : ScalarField) (m_squared : ℝ) (g : MetricTensor) (vol : VolumeElement) : ℝ :=
proof body
Definition body.
50 (m_squared / 2) * integrate_scalar (field_squared φ) g vol
51
52/-- Integration is linear (finite weighted sum).
53 STATUS: PROVED — Linearity of finite sums. -/
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
-
PsiKinetic
in IndisputableMonolith.Relativity.ILG.Action
decl_use
-
PsiPotential
in IndisputableMonolith.Relativity.ILG.Action
decl_use
depends on (20)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
MetricTensor
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
MetricTensor
in IndisputableMonolith.Gravity.Connection
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
MetricTensor
in IndisputableMonolith.Meta.Homogenization
decl_use
-
ScalarField
in IndisputableMonolith.NavierStokes.DiscreteNSOperator
decl_use
-
integrate_scalar
in IndisputableMonolith.Relativity.Fields.Integration
decl_use
-
VolumeElement
in IndisputableMonolith.Relativity.Fields.Integration
decl_use
-
field_squared
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
ScalarField
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use
-
MetricTensor
in IndisputableMonolith.Relativity.Geometry.Metric
decl_use
-
ScalarField
in IndisputableMonolith.Relativity.Geometry.Tensor
decl_use
-
VolumeElement
in IndisputableMonolith.Relativity.ILG.Action
decl_use