pith. sign in
module module high

IndisputableMonolith.Relativity.Fields.Integration

show as:
view Lean formalization →

The module supplies the volume element d⁴x equipped with metric measure √(-g) for covariant spacetime integrals of scalar fields. It aggregates supporting definitions that enable action functionals in relativistic settings. Field theorists cite the module when constructing invariant integrals over four-dimensional manifolds. The module consists entirely of definitions with no proofs.

claimThe invariant volume element is $d^4x sqrt(-g)$, where $g=det(g_{mu nu})$, used to form integrals of scalar fields $phi$ as $int d^4x sqrt(-g) L(phi)$ with Lagrangian density $L$.

background

The module operates inside the relativistic fields portion of the Recognition framework. It imports the Scalar module, whose doc comment states that a scalar field assigns a real value to each spacetime point, and the Geometry module, which re-exports manifold and metric components. The module doc comment identifies its central object as the volume element d⁴x with metric measure √(-g) to guarantee diffeomorphism invariance.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by the Fields aggregator that re-exports all field-related definitions. It supplies the integration primitives required by sibling declarations for kinetic_action, potential_action, and einstein_hilbert_action.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)