pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Relativity.Fields.Integration

show as:
view Lean formalization →

The Integration module defines the spacetime volume element d⁴x with metric measure √(-g) and supplies integration operators for scalar fields. It supports construction of kinetic, potential, and Einstein-Hilbert actions in curved spacetime. Physicists formalizing Recognition Science field theories cite these when deriving action integrals from the forcing chain. The module consists of definitions and lemmas with no core proofs.

claimThe volume element is $d^4x$ equipped with the metric measure factor $√(-g)$, where $g=det(g_{μν})$. Scalar field integration is defined via operators such as $∫ ϕ d^4x √(-g)$ for a scalar field ϕ that assigns a real value to each spacetime point.

background

This module sits inside the Recognition Science derivation of physics from the single functional equation, specifically the T5 J-uniqueness relation and the Recognition Composition Law. It imports scalar fields, each of which assigns a real value to every spacetime point, and the geometry aggregator that re-exports metric and coordinate structures. The volume element incorporates √(-g) to guarantee diffeomorphism invariance, aligning with the phi-ladder mass formulas and the eight-tick octave period.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Relativity.Fields aggregator, which re-exports all field-related definitions for use in higher-level constructions such as the UnifiedForcingChain and the T8 derivation of D=3 spatial dimensions. It supplies the integration measure required for the Einstein-Hilbert action and kinetic terms that appear in the mass formula yardstick * phi^(rung-8+gap(Z)).

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)