pith. sign in
module module high

IndisputableMonolith.Relativity.Geodesics.NullGeodesic

show as:
view Lean formalization →

This module defines null geodesics as curves with zero interval length using an affine parameter lambda in the Recognition Science relativity setting. Physicists modeling light-like propagation or geodesic uniqueness in Minkowski and curved backgrounds would reference these objects. It functions as an aggregator of geometry and calculus primitives with no internal proofs.

claimA null geodesic is a curve $C: I → M$ with interval $ds^2 = 0$ parameterized by affine parameter $λ$, satisfying the geodesic equation derived from the metric.

background

The module sits inside the Relativity namespace and imports the Geometry and Calculus aggregators. These upstream modules supply the differential geometry primitives and calculus operations needed to express interval length and affine reparameterization. The supplied doc-comment states the core object as a path with zero interval using lam for the affine parameter.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the base definitions for null geodesics that support later results on geodesic existence, uniqueness, and affine reparameterization within the Recognition Science framework. It contributes to the relativity development that ultimately connects to the forcing chain and physical constants derived from the Recognition Composition Law.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)