covariant_deriv_bilinear
plain-language theorem explainer
This definition supplies a placeholder covariant derivative for any bilinear form on a four-dimensional spacetime, always returning the zero map. Scaffold developers in the relativity geometry layer would reference it to close metric-compatibility checks. The body is a direct constant-zero function with no computation or dependence on the supplied metric or form.
Claim. The covariant derivative of a bilinear form $B$ along index direction $ρ$ with respect to metric tensor $g$ is the zero bilinear form: $∇_ρ B = 0$.
background
The Relativity.Geometry.Connection module is labeled a scaffold outside the verified certificate chain. It supplies placeholder definitions for Christoffel symbols and covariant derivatives, all defaulting to zero. BilinearForm is the local interface (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ, while MetricTensor is the corresponding structure carrying metric components g. Upstream MetricTensor and BilinearForm declarations appear in the Hamiltonian, Gravity.Connection, Meta.Homogenization, and Tensor modules as non-sealed local interfaces for the recognition-field scaffold.
proof idea
One-line definition that discards all three arguments and returns the constant zero bilinear form. No lemmas or tactics are invoked.
why it matters
The definition is the direct dependency of the metric_compatibility theorem in the same module, which states that the covariant derivative of the metric itself vanishes. It occupies a structural slot in the relativity geometry scaffolding but lies outside the core Recognition Science certificate chain. The module documentation explicitly cautions that these placeholders are not rigorous differential geometry and should not be cited as proven mathematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.