cov_deriv_1_2
plain-language theorem explainer
The covariant derivative for a (1,2) tensor field is defined componentwise via the metric connection and partial derivative. Differential geometers and relativists would cite it when expressing parallel transport or curvature action on mixed tensors. The definition assembles the standard formula by direct substitution of the Christoffel symbols and the placeholder partial derivative operator.
Claim. $∇_ρ T^λ_{μν} = ∂_ρ T^λ_{μν} + Γ^λ_{ρσ} T^σ_{μν} - Γ^σ_{ρμ} T^λ_{σν} - Γ^σ_{ρν} T^λ_{μσ}$, where Γ denotes the Christoffel symbols of the metric tensor g.
background
The declaration sits in the Relativity.Geometry.CovariantDerivative module, which builds tensor calculus on a 4-dimensional manifold using the local MetricTensor structure as a bilinear form interface. The Christoffel symbols are supplied by the upstream christoffel definition, originally stated for the Hessian metric g(x) = 1/x³ with explicit value -3/(2x) in one dimension. Partial differentiation is routed through the placeholder partialDeriv_v2 from the Hamiltonian module, which returns zero in its current scaffold form.
proof idea
The definition first binds Γ to the Christoffel symbols of g at x. It then adds the partial derivative of the tensor component in the rho direction, plus the single contraction on the upper index, and subtracts the two contractions on the lower indices. This is a direct term-by-term transcription of the coordinate formula for the covariant derivative on a (1,2) tensor.
why it matters
The definition supplies the missing (1,2) case in the covariant derivative hierarchy needed for curvature and field equations inside the Recognition Science geometry layer. It directly implements the formula quoted in its own doc-comment and thereby closes one step toward the full tensor calculus required by the relativity sector. No downstream uses are recorded yet, so it functions as an interface definition awaiting higher-level applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.