covariant_deriv_bilinear
This definition supplies a placeholder covariant derivative for bilinear forms that returns the zero map in all cases. It supports metric compatibility checks inside the relativity geometry scaffold. The implementation is a direct constant function assignment with no dependence on the input metric, form, or index.
claimThe covariant derivative of a bilinear form $B$ is the zero bilinear form: $B(x,y) = 0$ for all vectors $x,y$.
background
MetricTensor is a structure whose field g holds a bilinear form representing metric components at each spacetime point. BilinearForm is an abbreviation for the map (Fin 4 → ℝ) → (Fin 4 → ℝ) → (Fin 2 → Fin 4) → ℝ, a local non-sealed interface for tensorial objects. The module is labeled a scaffold that supplies zero defaults for Christoffel symbols and covariant derivatives; its module doc states these are structural placeholders, not rigorous differential geometry, and should not be cited as proven mathematics. Upstream MetricTensor and BilinearForm declarations from Hamiltonian and Tensor supply the type signatures used here.
proof idea
One-line definition that directly assigns the constant zero function to all inputs, ignoring the metric, the bilinear form, and the direction index.
why it matters in Recognition Science
The definition is invoked by the downstream metric_compatibility theorem, which concludes that the covariant derivative of the metric itself vanishes. It occupies the relativity geometry layer as a temporary scaffold outside the certificate chain. The module doc explicitly flags the entire file as non-certificate material.
scope and limits
- Does not implement a non-zero covariant derivative or connection.
- Does not reference Christoffel symbols or any curvature terms.
- Does not apply to general manifolds or non-flat metrics.
- Does not satisfy differential identities beyond the zero assignment.
Lean usage
theorem metric_compatibility (g : MetricTensor) : ∀ ρ x up low, covariant_deriv_bilinear g g.g ρ x up low = 0 := by intro ρ x up low; unfold covariant_deriv_bilinear; rflformal statement (Lean)
50noncomputable def covariant_deriv_bilinear (_g : MetricTensor)
51 (_B : BilinearForm) (_ρ : Fin 4) : BilinearForm := fun _ _ _ => 0
proof body
Definition body.
52
53/-- Metric compatibility: ∇_ρ g_μν = 0. -/