Prove IsKilling.length_sq_directional_eq_zero (Killing fields have constant length along their own flow)

[Xinze-Li-Moqian]

Statement to prove

OpenGALib/Riemannian/Curvature/RiemannCurvature.lean:839

theorem IsKilling.length_sq_directional_eq_zero
    (X : SmoothVectorField I M) (_hX : IsKilling X) (x : M) :
    directionalDeriv (fun y => ⟪X y, X y⟫_g) x (X x) = 0 := by
  sorry

Math

For a Killing field $X$,

$$X \cdot g(X, X) = 0.$$

Equivalently, $|X|^2_g : M \to \mathbb{R}$ has zero directional derivative along $X$, so $|X|^2_g$ is constant along each integral curve of $X$. The infinitesimal expression of "isometries preserve length".

Repair plan (sketched in the docstring)

By the product rule for mfderiv and metric compatibility of covDeriv,
$$X \cdot g(X, X) = 2, g(\nabla_X X, X).$$
The Killing equation with $U = W = X$ reads $g(\nabla_X X, X) + g(\nabla_X X, X) = 0$, i.e. $g(\nabla_X X, X) = 0$.

Estimated 40–60 LOC.

Ground truth

• do Carmo §3 Ex. 5 (b)
• Petersen Ch. 8 §2