Add riem_simp attribute + riem_normalize tactic; polish riemannCurvature_antisymm

Engineering layer (Util/) gains its first real Riemann-tensor
infrastructure. The polish target on riemannCurvature_antisymm shrinks
12 lines → 3 lines while preserving the same mathematical content,
demonstrating the API design pattern for downstream curvature work.

Util/ additions:
- Util/Attributes.lean: register_simp_attr riem_simp (paralleling
  metric_simp). Declaration only — populated by lemmas in math files.
- Util/Tactic.lean: macro "riem_normalize" : tactic => simp only
  [riem_simp]. Real executable tactic in Util, not just docstrings.

Math layer (Connection/Bianchi.lean) additions:
- riemannCurvature_unfold (@[riem_simp]): definitional expansion of
  R(X,Y)Z to ∇∇ - ∇∇ - ∇_{[·,·]} form, rfl proof.
- covDeriv_lambda_mlieBracket_swap: pulls Lie-bracket antisymmetry
  through covDeriv's direction argument. Kept OUT of riem_simp to
  avoid X ↔ Y rewrite loop; used as explicit rw step.

Polished proof of riemannCurvature_antisymm: 3 lines (simp / rw / abel),
each a single math step. Build verified (3514 jobs).

Author: Xinze-Li-Moqian

OpenGALib/Riemannian/Connection/Bianchi.lean

@@ -1,4 +1,5 @@
 import OpenGALib.Riemannian.Connection.LeviCivita
+import OpenGALib.Riemannian.Util.Attributes
 
 /-!
 # Riemannian.Connection.Bianchi
@@ -162,28 +163,56 @@ noncomputable def riemannCurvature
   let bracketXY : Π x : M, TangentSpace I x := fun x => mlieBracket I X Y x
   covDeriv X nablaYZ x - covDeriv Y nablaXZ x - covDeriv bracketXY Z x
 
+/-! ### `riem_simp` lemmas
+
+Two rewrites that drive the `riem_simp` simp set, populated for the
+Riemann curvature operator built from the framework's `covDeriv`. Together
+with `abel` they discharge the algebraic identities of `riemannCurvature`
+without exposing the underlying connection plumbing. -/
+
+/-- **Definitional unfold** of `riemannCurvature` to the
+$\nabla \nabla - \nabla \nabla - \nabla_{[\cdot,\cdot]}$ form.
+Pure rewrite — no smoothness hypotheses. -/
+@[riem_simp]
+theorem riemannCurvature_unfold
+    (X Y Z : Π x : M, TangentSpace I x) (x : M) :
+    riemannCurvature X Y Z x
+      = covDeriv X (fun y => covDeriv Y Z y) x
+        - covDeriv Y (fun y => covDeriv X Z y) x
+        - covDeriv (fun y => mlieBracket I X Y y) Z x := rfl
+
+/-- **Lie-bracket antisymmetry pulled through the connection's direction
+argument**: $\nabla_{[Y,X]} Z = -\nabla_{[X,Y]} Z$ pointwise. Combines
+`VectorField.mlieBracket_swap_apply` with the ℝ-linearity of
+`leviCivitaConnection.toFun Z x` (a CLM, so it commutes with negation).
+Pure rewrite — no smoothness hypotheses.
+
+Used as an explicit `rw` step (not in `riem_simp`): the rewrite is
+symmetric in `X ↔ Y`, so adding it to a simp set causes loop. -/
+theorem covDeriv_lambda_mlieBracket_swap
+    (X Y Z : Π x : M, TangentSpace I x) (x : M) :
+    covDeriv (fun y => mlieBracket I Y X y) Z x
+      = -covDeriv (fun y => mlieBracket I X Y y) Z x := by
+  unfold covDeriv
+  rw [show (fun y => mlieBracket I Y X y) x = -mlieBracket I X Y x from
+        VectorField.mlieBracket_swap_apply,
+      (leviCivitaConnection.toFun Z x).map_neg]
+
 /-- **Riemann tensor antisymmetry in the first two arguments**:
 $R(X, Y) Z = -R(Y, X) Z$ pointwise.
 
-Direct from antisymmetry of the Lie bracket
-(`VectorField.mlieBracket_swap_apply`) plus ℝ-linearity of
-`leviCivitaConnection.toFun Z z` (it is a CLM).
+Math: Lie bracket is antisymmetric and the connection is linear in its
+direction argument. `simp only [riem_simp]` unfolds `R` to its
+$\nabla \nabla - \nabla \nabla - \nabla_{[\cdot,\cdot]}$ form;
+`covDeriv_lambda_mlieBracket_swap` pulls the bracket-swap negation
+through `covDeriv`; `abel` finishes.
 
 **Ground truth**: do Carmo 1992 §4 Proposition 2.5 (i). -/
 theorem riemannCurvature_antisymm
     (X Y Z : Π x : M, TangentSpace I x) (x : M) :
     riemannCurvature X Y Z x = -riemannCurvature Y X Z x := by
-  show covDeriv X (fun y => covDeriv Y Z y) x
-        - covDeriv Y (fun y => covDeriv X Z y) x
-        - covDeriv (fun y => mlieBracket I X Y y) Z x
-      = -(covDeriv Y (fun y => covDeriv X Z y) x
-            - covDeriv X (fun y => covDeriv Y Z y) x
-            - covDeriv (fun y => mlieBracket I Y X y) Z x)
-  have h_swap : mlieBracket I Y X x = -mlieBracket I X Y x :=
-    VectorField.mlieBracket_swap_apply
-  unfold covDeriv
-  rw [show (fun y => mlieBracket I Y X y) x = -mlieBracket I X Y x from h_swap,
-      (leviCivitaConnection.toFun Z x).map_neg]
+  simp only [riem_simp]
+  rw [covDeriv_lambda_mlieBracket_swap]
   abel
 
 /-! ## Algebraic Bianchi I

OpenGALib/Riemannian/Util/Attributes.lean

@@ -19,3 +19,11 @@ rules, zero / neg / sub / self_nonneg. Tagged on the lemmas in
 `Metric/Basic.lean`; downstream proofs can invoke
 `simp only [metric_simp]` for routine inner-product calculations. -/
 register_simp_attr metric_simp
+
+/-- Simp set for `riemannCurvature` algebra normalisation: definitional
+unfold ($R(X,Y)Z = \nabla_X \nabla_Y Z - \nabla_Y \nabla_X Z - \nabla_{[X,Y]} Z$),
+Lie-bracket antisymmetry under `covDeriv`, and connection-direction
+linearity rewrites. Tagged on lemmas in `Connection/Bianchi.lean`;
+downstream proofs invoke `simp only [riem_simp]` to normalise curvature
+expressions before `abel` / `ring` / further reasoning. -/
+register_simp_attr riem_simp

OpenGALib/Riemannian/Util/Tactic.lean

@@ -20,18 +20,42 @@ metric algebra lemmas tagged with them.
     `metricInner_sub_left/right`, `metricInner_add_left/right`,
     `metricInner_smul_left/right`, `metricInner_self_nonneg`.
 
+  * `riem_simp` — `riemannCurvature` algebra normalisation. Currently
+    populated by `riemannCurvature_unfold` (definitional expansion to
+    `∇∇ - ∇∇ - ∇_{[·,·]}` form, no smoothness hypotheses). Use with
+    explicit `rw` of the bracket-swap helper
+    `covDeriv_lambda_mlieBracket_swap` (kept out of the simp set to
+    avoid `X ↔ Y` rewrite loops) and `abel` to close Riemann-tensor
+    algebraic identities.
+
+## Tactics
+
+  * `riem_normalize` — shorthand for `simp only [riem_simp]`. Use as a
+    first step on goals involving `riemannCurvature`; pair with explicit
+    `rw` of named bracket / linearity lemmas as needed.
+
 ## Usage
 
 ```
 example {g : RiemannianMetric I M} (x : M) (V : TangentSpace I x) :
     metricInner x (V - 0) (-V + V) = -metricInner x V V + metricInner x V V := by
   simp only [metric_simp]
+
+example (X Y Z : Π x : M, TangentSpace I x) (x : M) :
+    riemannCurvature X Y Z x = -riemannCurvature Y X Z x := by
+  riem_normalize
+  rw [covDeriv_lambda_mlieBracket_swap]
+  abel
 ```
 
 ## Future extensions (deferred)
 
   * `koszul_simp` — Koszul algebraic identities.
-  * `riem_simp` — Riemann tensor algebra.
   * `metric_calc` — bespoke tactic combining `metric_simp` with `ring`
     for closed-form algebraic goals.
 -/
+
+/-- **`riem_normalize` tactic** — applies the `riem_simp` simp set to
+normalise `riemannCurvature` expressions to their underlying
+`∇∇ - ∇∇ - ∇_{[·,·]}` form. Equivalent to `simp only [riem_simp]`. -/
+macro "riem_normalize" : tactic => `(tactic| simp only [riem_simp])