IndisputableMonolith.Relativity.Geometry.CovariantDerivative
This module defines the covariant derivative for a (1,2) tensor in the relativity geometry layer. It would be cited by any derivation requiring parallel transport or curvature effects on tensors. The module is purely definitional and assembles the standard formula from imported Christoffel symbols and partial derivatives.
claimThe covariant derivative of the (1,2) tensor $T^\lambda_{\mu\nu}$ is $\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}$.
background
The module sits in the Relativity.Geometry section and imports the standard basis from Derivatives, Christoffel symbols from Curvature (derived from the metric), and tensor structures from Tensor. The Tensor module is explicitly marked as scaffolding outside the certificate chain. The supplied doc-comment states the explicit coordinate expression for the covariant derivative of a (1,2) tensor.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the covariant derivative operator required for tensor calculus in the relativity domain. No downstream declarations are recorded in the used_by edges, so it currently stands as an isolated definition block supporting the geometry layer.
scope and limits
- Does not define covariant derivatives for tensors of other ranks.
- Does not prove metric compatibility or vanishing torsion.
- Does not link the definition to the Recognition Science forcing chain or phi-ladder.