module module high

`IndisputableMonolith.Relativity.Fields.Scalar`

This module defines scalar fields on spacetime, each assigning a real value to every point. Field theorists in the Recognition framework import it to construct potentials and matter fields before adding integration or dynamics. It consists of the ScalarField type plus basic operations including evaluation, constants, addition, scalar multiplication, and directional derivatives.

claimA scalar field on spacetime is a map $f: M → ℝ$ where $M$ denotes the spacetime manifold; the module supplies the type together with evaluation, constant fields, addition, scalar multiplication, and directional derivatives.

background

The module resides in the Relativity domain and imports the Geometry aggregator, which re-exports all geometric primitives. Its central definition is the ScalarField type, a function from spacetime points to the reals, equipped with pointwise evaluation, constant fields, addition, scalar multiplication, and directional derivatives. These constructions sit upstream of any field dynamics or integration.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the scalar-field primitives consumed by the Fields aggregator and by the Integration module, which implements volume integration with the √(-g) measure. The definitions close the basic algebraic layer before any Recognition-specific structures such as J-cost or the phi-ladder are attached.

scope and limits

Does not define vector or tensor fields.
Does not implement integration measures or volume forms.
Does not reference J-cost, defectDist, or the phi-ladder.
Does not connect to the eight-tick octave or spatial dimension forcing.

used by (2)

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

IndisputableMonolith.Relativity.Fields module_import
IndisputableMonolith.Relativity.Fields.Integration module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Relativity.Geometry module_import

declarations in this module (19)

structure ScalarField L11
def eval L15
def constant L18
theorem constant_eval L20
def zero L24
theorem zero_eval L26
def add L29
def smul L33
theorem add_comm L36
theorem smul_zero L42
def directional_deriv L48
theorem deriv_add L54
theorem deriv_smul L60
theorem deriv_constant L66
def gradient L72
def gradient_squared L76
theorem gradient_squared_minkowski L83
def field_squared L90
theorem field_squared_nonneg L93