Prove IsKilling.divergence_eq_zero (Killing fields are divergence-free)

[Xinze-Li-Moqian]

Statement to prove

OpenGALib/Riemannian/Operators/Divergence.lean:103

theorem IsKilling.divergence_eq_zero
    (X : SmoothVectorField I M) (_hX : IsKilling X) (x : M) :
    div_g[I] X x = 0 := by
  sorry

Math

Killing vector fields are divergence-free:

$$\mathrm{div}_g X(x) = 0 \quad \text{for every Killing } X.$$

The infinitesimal form of "isometries preserve volume". Foundation for Bochner–Yano isometry-group dimension bounds and rigidity of Killing fields on closed manifolds with positive Ricci curvature.

Repair plan (sketched in the docstring)

Trace the Killing equation
$$g(\nabla_U X, W) + g(\nabla_W X, U) = 0$$
with $U = W = \varepsilon_i$, summed over the $g$-orthonormal frame. Each diagonal term equals $2 g(\nabla_{\varepsilon_i} X, \varepsilon_i)$, so $2 \mathrm{div}_g X = 0$.

1. Unfold divergence to its smoothOrthoFrame form.
2. Apply hX (B_i) (B_i) x for each frame vector.
3. Sum the resulting cancellations.

Estimated 40–60 LOC.

Ground truth

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