Prove bianchi_second (differential Bianchi identity)

[Xinze-Li-Moqian]

Current state

OpenGALib/Riemannian/Connection/LeviCivita.lean :: bianchi_second is statement-only (sorry'd). The statement:

```lean
theorem bianchi_second
[IsManifold I 3 M]
(X Y Z W : SmoothVectorField I M) (x : M) :
(∇R)[X](Y, Z) W x + (∇R)[Y](Z, X) W x + (∇R)[Z](X, Y) W x = 0 := by
sorry
```

This is the differential Bianchi identity — the cyclic sum of covariant derivatives of the Riemann curvature tensor vanishes. Standard textbook (do Carmo Ch.4, Petersen Ch.3, Cheeger–Ebin Thm 1.4).

Repair plan (already in docstring)

The standard proof composes:

1. Commutator form of Riem — riemannCurvature_commutator_form
2. covDeriv distributivity — covDeriv_add_field, covDeriv_sub_field
3. First Bianchi identity — bianchi_first (already proven at LeviCivita.lean:745)
4. Manifold Lie-bracket Jacobi — SmoothVectorField.mlieBracket_jacobi

Concrete steps (adapted from synthetic-DG Connection.lean:348 in external repo):

• Expand (∇R) into 12 covDeriv ∘ covDeriv ∘ covDeriv terms
• Group into 6 pairs via subtractivity of covDeriv in the first slot
• Reduce each pair to an mlieBracket term via torsion-freeness
• Close via Jacobi

Why it's reasonable to do

• Infrastructure in place: bianchi_first, riemannCurvature_commutator_form, covDeriv_*_field, mlieBracket_jacobi all already proven.
• Pure mechanical algebraic manipulation, no Mathlib gap.
• Reference proof exists in external differential-geometry repo.

Estimated scope

~80-120 LOC. Multi-session but tractable.

Acceptance

• bianchi_second 0 sorries
• docs/SORRY_CATALOG.md updated (Riemannian count decreases by 1)
• CI EXPECTED decreases by 1

See also

docs/SORRY_CATALOG.md row at Connection.lean:956. (Note: the line number in the catalog is stale — the actual location is LeviCivita.lean:921. Catalog row should also be updated.)