Prove bianchi_second

[dxww123]

Closes #12.

Summary

Proves OpenGALib/Riemannian/Connection/LeviCivita.lean :: bianchi_second and closes the remaining statement-only sorry for the differential Bianchi identity.

The implementation takes a connection-algebra route:

• expands covDerivRiemann into the torsion-free commutator form of curvature
• groups the six connection-difference pairs into Lie-bracket terms via covDeriv_sub_swap_eq_mlieBracket
• collapses the grouped terms using section-level torsion-freeness rewrites
• finishes with SmoothVectorField.mlieBracket_jacobi

It also updates the CI sorry baseline from EXPECTED=36 to EXPECTED=35.

Validation

• lake build OpenGALib.Riemannian.Connection.LeviCivita
• sorry count regex over OpenGALib/**/*.lean: 35

[Xinze-Li-Moqian]

已直接帮忙 rebase + 解决冲突,不需要你再改了。说明一下改了什么:

main 上的 9g 重构(#38/#39/#40)在此 PR 分叉后,已经把 covDerivRiemann 迁成 explicit-HasMetric.metric 形式,并删掉了 ∇[X] Y / (∇R)[X](Y,Z) W / Riem(Y,Z) W 这些 typeclass-dispatch 记号(详见 Util/Notation.lean)。所以本 PR 与 main 冲突。

冲突解决方式(merge commit eff7ac0):

• 保留你这条无挠对易子展开的定义和整套证明(bianchi_second 正是对着这个展开式证的);
• 仅把废弃记号翻译成 explicit-g:
  • ∇[A] B → covDeriv HasMetric.metric A B
  • (∇R)[X](Y, Z) W → covDerivRiemann X Y Z W
  • ⟦·,·⟧(Lie 括号)9g 保留,未动;
• .github/workflows/ci.yml 的 sorry baseline 自动合并为 EXPECTED=35。

验证:整库 lake build 通过(3670 jobs),LeviCivita.lean 0-sorry,CI 口径全仓 sorry = 35。挂了 auto-merge,CI 绿后自动合入 main。