Prove IsKilling.second_covDeriv_eq_curvature (Killing field PDE)

[Xinze-Li-Moqian]

Current state

OpenGALib/Riemannian/Curvature/RiemannCurvature.lean :: IsKilling.second_covDeriv_eq_curvature is statement-only (sorry'd, commit 62bfea6):

```lean
theorem IsKilling.second_covDeriv_eq_curvature
(X : SmoothVectorField I M) (_hX : IsKilling X)
(Y Z : SmoothVectorField I M) (x : M) :
(∇[Y] (∇[Z] X)) x - (∇[∇[Y] Z] X) x = Riem(X, Y) Z x := by
sorry
```

This is the defining PDE of infinitesimal isometries: a Killing field's second covariant derivative equals the Riemann curvature acting on itself. Foundation for:

• The Bochner–Yano dimension bound: dim Isom(M) ≤ n(n+1)/2
• Rigidity of constant-curvature manifolds
• The isometry-group Lie-algebra structure
• Symmetric-space classification

Repair plan (per docstring)

The standard proof composes:

1. Killing equation at three points (the hypothesis _hX : IsKilling X says g(∇_U X, W) + g(∇_W X, U) = 0 for all U, W and point y).
2. Metric compatibility (covDeriv_metric_compat or equivalent in LeviCivita.lean).
3. Curvature commutator identity (riemannCurvature_def).

Concrete sketch:

• Differentiate Killing equation along a third direction Y: Y(g(∇_Z X, W)) + Y(g(∇_W X, Z)) = 0.
• Apply metric compatibility to expand Y(g(·, ·)) into g(∇_Y ·, ·) + g(·, ∇_Y ·).
• Permute the roles of Y, Z, W to get three versions of the differentiated equation.
• Combine to isolate ∇²_{Y, Z} X.
• The curvature commutator R(Y, Z) X = ∇_Y ∇_Z X - ∇_Z ∇_Y X - ∇_{[Y, Z]} X enters when symmetrizing.

The bulk of the work is sign-bookkeeping across the 6 permutations.

Infrastructure in place

• IsKilling definition (RiemannCurvature.lean:795)
• covDeriv (LeviCivita.lean)
• riemannCurvature (LeviCivita.lean)
• mlieBracket I (Mathlib smooth Lie bracket)
• riemannCurvature_def (curvature commutator unfolding)
• metricInner algebra (Metric/RiemannianMetric.lean)
• Metric compatibility of covDeriv (LeviCivita.lean)

All necessary lemmas exist; the proof is composition + permutation + algebra.

Estimated scope

80-120 LOC. Multi-session but tractable. Pure mechanical algebra once the proof outline is laid out — no Mathlib gap.

Mathematical references

• do Carmo, Riemannian Geometry, Ch. 3 Ex. 5
• Petersen, Riemannian Geometry 3rd ed., Ch. 8 §2 (Prop 8.1.1)
• Cheeger–Ebin, Comparison Theorems in Riemannian Geometry, §1.84
• Kobayashi–Nomizu, vol. I, Ch. III §2

Convention note

OpenGA's curvature convention is R(X, Y) Z := ∇_X ∇_Y Z - ∇_Y ∇_X Z - ∇_{[X, Y]} Z (matches Petersen). Do Carmo uses the opposite sign convention — when porting do Carmo's proof, flip R-signs accordingly. The target identity is stated in OpenGA convention.

Acceptance

• IsKilling.second_covDeriv_eq_curvature 0 sorries.
• docs/SORRY_CATALOG.md updated (Riemannian count decreases by 1).
• CI EXPECTED decreases by 1.
• Build clean, all linters at baselines.

Why this is a good "math practice" task

Same difficulty profile as #12 (bianchi_second): mechanical-algebraic proof, all infrastructure already in position, statement clean and classical, opens a new substantive line (Killing/isometry theory). Independent of the main explicit-g cascade (#9) — can be done by a different contributor in parallel.

See also

• Prove bianchi_second (differential Bianchi identity) #12 (sibling task: bianchi_second, also statement-only, same difficulty profile, also currently unassigned for a future contributor).