IndisputableMonolith.Relativity.Fields
This module supplies scalar field definitions and spacetime volume integration for relativistic models in Recognition Science. Workers on compact solutions, gravitational waves, and ILG actions import it to build field content and measures. It consists of two submodules: one assigning real values to spacetime points and one approximating integrals with the √(-g) element via discrete methods.
claimA scalar field is a map $M → ℝ$ from spacetime $M$ to the reals. Volume integration uses the measure $√(-g) d^4x$ implemented via discrete approximation.
background
The module resides in the Relativity domain and re-exports two submodules. Scalar assigns a real value to each spacetime point. Integration implements volume integration with the √(-g) measure; its doc states it uses discrete approximation and notes that a full version would employ Mathlib measure theory.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
It supplies the field and integration primitives required by StaticSpherical for compact solutions, by GW.ActionExpansion for gravitational wave actions, and by ILG.Action for re-exporting geometry and field types in the ILG framework.
scope and limits
- Does not implement continuous integration via Mathlib measure theory.
- Does not define vector, tensor, or spinor fields.
- Does not include field equations, Lagrangians, or dynamics.
- Does not specify spacetime metrics beyond the volume element.