def definition def or abbrev

`default_volume`

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

formal statement (Lean)

  26noncomputable def default_volume : VolumeElement :=

proof body

Definition body.

  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. -/

used by (2)

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

PsiKinetic in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiPotential in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (3)

Lean names referenced from this declaration's body.

kinetic_action in IndisputableMonolith.Relativity.Fields.Integration decl_use
VolumeElement in IndisputableMonolith.Relativity.Fields.Integration decl_use
VolumeElement in IndisputableMonolith.Relativity.ILG.Action decl_use