VolumeElement
VolumeElement re-exports the grid-based volume structure for discrete spacetime integrals in the ILG action. Researchers constructing Einstein-Hilbert or kinetic actions cite it to supply the measure factor in integration lemmas. The declaration is a direct one-line alias to the structure defined in the Fields module.
claimLet $V$ denote the volume element structure consisting of a grid spacing parameter satisfying $0 < grid_spacing$, used to approximate the spacetime measure $d^4x$ with metric factor $sqrt(-g)$ in discrete sums.
background
The ILG.Action module re-exports geometry and field types to support action integrals. VolumeElement is an alias to the structure imported from Fields.Integration, which carries a positive real grid spacing for uniform sampling. This structure is required by integrate_scalar, which computes a finite sum over grid points weighted by the metric factor.
proof idea
The declaration is a one-line alias to the VolumeElement structure from IndisputableMonolith.Relativity.Fields.Integration.
why it matters in Recognition Science
It supplies the volume measure required by einstein_hilbert_action, kinetic_action, and eh_action_minkowski. These feed the discrete approximation to the Einstein-Hilbert integral in the Relativity section of the Recognition framework. The alias closes a re-export step so that action definitions remain consistent when the integration machinery is extended.
scope and limits
- Does not perform any integration or summation.
- Does not specify a metric tensor or curvature scalar.
- Does not enforce a continuous spacetime limit.
- Does not incorporate J-cost, phi-ladder, or core Recognition constants.
formal statement (Lean)
12abbrev VolumeElement := Fields.VolumeElement
proof body
Definition body.
13
14/-- Einstein–Hilbert action: S_EH = (M_P²/2) ∫ √(-g) R d^4x.
15 Scaffold: returns symbolic R evaluation (integration machinery pending). -/