covariant_deriv_covector
plain-language theorem explainer
This placeholder definition sets the covariant derivative of any covector field to the zero field in the Recognition Science relativity geometry module. It would be referenced in constructions of flat spacetime connections or trivial parallel transport. The body is a constant function that ignores its arguments and returns zero everywhere, matching the scaffold status of the module.
Claim. The covariant derivative of a covector field with respect to a metric tensor is defined to be the zero covector field.
background
The module supplies placeholder definitions for Christoffel symbols and covariant derivatives in a relativity geometry layer. MetricTensor is a structure providing a local bilinear form on Fin 4 indices, with components defaulting to zero in one upstream interface and a symmetric matrix in another. Covector fields are sections of the cotangent bundle abstracted over these indices. The module documentation states that all such derivatives collapse to zero as structural stand-ins, outside the verified certificate chain and unrelated to J-cost or phi-ladder structures from upstream results such as PhiForcingDerived and SpectralEmergence.
proof idea
The definition is a direct one-line constant that returns the zero covector field regardless of the metric, input field, or index. No lemmas or tactics are invoked; the implementation simply ignores all parameters.
why it matters
This definition supplies a temporary typed interface in the relativity geometry layer so that downstream constructions can reference a covariant derivative operator. It has no downstream uses and sits explicitly outside the certificate chain. In the broader framework it would need replacement by a non-trivial connection derived from the metric compatibility condition once the placeholder is discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.