def definition def or abbrev

`EHAction`

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

formal statement (Lean)

  16noncomputable def EHAction (g : Metric) : ℝ :=

proof body

Definition body.

  17  -- Placeholder integration over spacetime volume
  18  -- Should be: integral over manifold of √(-g(x)) * R(x)
  19  let x₀ : Fin 4 → ℝ := fun _ => 0  -- Sample point
  20  Geometry.ricci_scalar g x₀  -- Scaffold: use single-point value
  21
  22/-- Alias for consistency. -/

used by (1)

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

S_EH in IndisputableMonolith.Relativity.ILG.Action decl_use

depends on (11)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
volume in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
ricci_scalar in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
Metric in IndisputableMonolith.Relativity.ILG.Action decl_use