Pith. sign in
module module high

IndisputableMonolith.Relativity.Calculus

show as:
view Lean formalization →

The Relativity.Calculus module supplies differential calculus infrastructure for spacetime calculations within Recognition Science. It imports the Derivatives submodule that defines the standard basis vector e_μ. Researchers deriving null geodesics, FRW metrics, or post-Newtonian expansions cite this module for coordinate manipulations. This is a definition module with no proofs.

claimThe module provides the differential calculus framework on the spacetime manifold equipped with the standard basis $e_\mu$ in the tangent space.

background

This module belongs to the Relativity domain and imports only IndisputableMonolith.Relativity.Calculus.Derivatives. The upstream doc-comment states that Derivatives supplies the 'Standard basis vector e_μ.' The local setting is coordinate-based differential geometry supporting derivations of relativistic effects from the J-cost and phi-ladder structures of the parent framework.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by StaticSpherical, FRWMetric, NullGeodesic, and Metric1PN. NullGeodesic uses it as foundation for computing gravitational lensing deflection angles and time delays; Metric1PN uses it for post-Newtonian potentials. It fills the calculus layer required by the T8 spatial-dimension and geodesic constructions in the forcing chain.

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.