IndisputableMonolith.Relativity.Geometry.CovariantDerivative
The CovariantDerivative module defines the covariant derivative for a (1,2) tensor in the Recognition Science relativity geometry. Researchers extending tensor calculus to curved spacetime in this framework would cite it when handling connections. The module supplies a single definition implementing the standard formula with partial derivatives and Christoffel symbols, with no proofs present.
claimThe covariant derivative of a (1,2) tensor $T$ is defined by $nabla_rho T^lambda_{mu nu} = partial_rho T^lambda_{mu nu} + Gamma^lambda_{rho sigma} T^sigma_{mu nu} - Gamma^sigma_{rho mu} T^lambda_{sigma nu} - Gamma^sigma_{rho nu} T^lambda_{mu sigma}$, where $Gamma$ denotes the Christoffel symbols.
background
This module resides in the Relativity.Geometry namespace and imports the Tensor, Curvature, and Derivatives modules from the same package plus Mathlib. The Curvature module supplies the Christoffel symbols derived from the metric. The Derivatives module provides the standard basis vector $e_mu$. The Tensor module is explicitly marked as a scaffold and excluded from the certificate chain. The definition implements the standard covariant derivative transformation law for mixed tensors.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the covariant derivative definition required for tensor operations in the relativity section of the Recognition Science framework. It builds directly on the Christoffel symbols from the Curvature module. No downstream declarations are recorded as using it yet.
scope and limits
- Does not prove any identities or properties of the covariant derivative.
- Does not define the operator for tensor ranks other than (1,2).
- Does not link the definition to the forcing chain or phi-ladder constructions.
- Does not contain any theorems or Lean proofs.