pith. sign in
module module high

IndisputableMonolith.Relativity.Calculus

show as:
view Lean formalization →

Relativity.Calculus supplies the differential infrastructure for spacetime tensor operations. It imports the Derivatives submodule that defines the standard basis vector e_μ and related derivative structures. The module is imported by four downstream relativity components to support metric, geodesic, and post-Newtonian calculations. Its content consists entirely of definitions with no theorems or proofs.

claimThe module introduces the standard basis $e_μ$ and derivative operators $∂_μ$ acting on the spacetime metric $g_{μν}$ and its derived tensors.

background

The module sits inside the Relativity domain of Recognition Science and imports only the Derivatives submodule. That submodule supplies the standard basis vector $e_μ$ used for coordinate expansions of tensors. The local setting is a pseudo-Riemannian manifold equipped with metric $g_{μν}$, where ordinary and covariant derivatives are required for geodesic equations and curvature computations.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds StaticSpherical, FRWMetric, NullGeodesic, and Metric1PN. NullGeodesic uses it to implement $dx^μ/dλ$ with $g_{μν} dx^μ dx^ν = 0$ for light propagation and lensing. Metric1PN relies on it for post-Newtonian potentials. It therefore supplies the shared calculus layer for all metric-based calculations in the framework.

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.