IndisputableMonolith.Relativity.Fields.Integration
Defines the spacetime volume element √(-g) d⁴x and the integrals that turn scalar densities into actions. Supplies kinetic and potential actions for a real scalar field, plus the Einstein–Hilbert term and its Minkowski reduction. Anyone assembling a variational principle in the RS relativity stack cites this module. Content is largely definitional with elementary linearity and nonnegativity lemmas.
claimOn a spacetime with metric $g$, the volume element is $\sqrt{-g}\,d^4x$. For a scalar field $\phi$, the module defines $\int f\,\sqrt{-g}\,d^4x$, the kinetic action $\int \tfrac12(\nabla\phi)^2\sqrt{-g}\,d^4x$, a potential action, and the Einstein–Hilbert action $\int R\sqrt{-g}\,d^4x$, with the Minkowski specialization $g=\eta$.
background
In classical field theory on a Lorentzian manifold, actions are integrals of scalar densities against the metric volume form. The Geometry import supplies the metric and curvature tensors; the Scalar import supplies a real-valued field on spacetime points.
This module packages the measure-theoretic side: a volume element built from $\sqrt{-g}$, a discrete sample grid for concrete evaluation, and the integral of a scalar density. From those primitives it builds the standard kinetic and potential pieces of a scalar action and the Einstein–Hilbert gravitational action.
Notation follows GR convention: $g=\det(g_{\mu\nu})$, signature with $\sqrt{-g}>0$ in the Lorentzian sector, and reduction to Lebesgue measure when $g=\eta$.
proof idea
This is primarily a definition module. VolumeElement, sqrt_minus_g, integrate_scalar, kinetic_action, potential_action, and einstein_hilbert_action are introduced as defs. Linearity lemmas (integrate_add, integrate_smul) and kinetic_nonneg are short algebraic or positivity arguments on top of those defs. eh_action_minkowski specializes the EH integrand to flat space. No deep analytic existence theory is claimed.
why it matters in Recognition Science
Feeds the Fields aggregator (IndisputableMonolith.Relativity.Fields), which re-exports all field-related definitions for the relativity stack. Without a coherent volume measure and action functionals, variational derivations of field equations and coupling to curvature cannot be stated inside the monolith. The Einstein–Hilbert piece and its Minkowski reduction anchor the gravitational sector next to the scalar kinetic/potential terms, so downstream modules can treat matter and geometry actions uniformly.
scope and limits
- Does not prove existence of continuum integrals on general manifolds.
- Does not derive Euler–Lagrange or Einstein equations from the actions.
- Does not fix a global topology or causal structure beyond the metric data.
- Does not address fermionic or gauge-field measures.
- Minkowski reduction does not cover curved-background perturbation theory.