pith. sign in
module module high

IndisputableMonolith.Relativity.Calculus

show as:
view Lean formalization →

The Relativity.Calculus module supplies the differential calculus layer for spacetime computations in Recognition Science. It is imported by modules on static spherical metrics, FRW cosmology, null geodesics, and post-Newtonian expansions. The module consists of one import to the Derivatives submodule that defines the standard basis vector.

claimThe module provides the standard basis vector $e_μ$ together with derivative operators for coordinate calculus on spacetime manifolds.

background

The module sits inside the Relativity domain and imports only the Derivatives submodule. That submodule's documentation states it supplies the standard basis vector $e_μ$. This notation supplies the coordinate frame used by all downstream relativity constructions. The local theoretical setting is the differential geometry required to express metrics, geodesics, and perturbations inside the Recognition Science framework.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds IndisputableMonolith.Relativity.Compact.StaticSpherical, IndisputableMonolith.Relativity.Cosmology.FRWMetric, IndisputableMonolith.Relativity.Geodesics.NullGeodesic (null geodesics for light propagation and lensing), and IndisputableMonolith.Relativity.PostNewtonian.Metric1PN (post-Newtonian potentials). It supplies the calculus primitives required for those metric and geodesic calculations.

scope and limits

used by (4)

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

depends on (1)

Lean names referenced from this declaration's body.