Riemannian: add manifoldGradient_smooth_of_smooth (PRE-PAPER)

Framework gradient-smoothness propagation lemma: g in C^inf implies
nabla g is C^inf as a tangent bundle section. Mathematically trivial in
standard differential geometry (composition of smooth mfderiv with
smooth Riesz isomorphism, since the Riemannian metric is smooth).

Closure path: shares the metricRiesz_section_smoothAt + chartGramMatrix
machinery with koszulCovDeriv_const_smoothAt (A.4-strong primitive).
Once that primitive lands, both lemmas close as one-line compositions.

Used by Bochner E (leibniz_trace_reduction) to discharge the automatic
smoothness of nabla(|nabla f|^2) — needed for the metric-compat
application against scalarLaplacian's hessian def.

Sorry: 34 -> 35 (PRE-PAPER, repair plan documented).

Author: Xinze-Li-Moqian

.github/workflows/ci.yml

@@ -22,7 +22,7 @@ jobs:
             --include="*.lean" \
             OpenGALib \
             2>/dev/null | wc -l | tr -d ' ')
-          EXPECTED=34
+          EXPECTED=35
           if [ "$ACTUAL" -ne "$EXPECTED" ]; then
             echo "::error::Sorry count drift: expected $EXPECTED, found $ACTUAL"
             echo "If the change is intentional, update docs/SORRY_CATALOG.md (and the EXPECTED constant in this workflow)."

OpenGALib/Riemannian/Gradient.lean

@@ -54,4 +54,29 @@ theorem manifoldGradient_inner_eq
     metricInner x (grad_g[I] f x) v = (mfderiv I 𝓘(ℝ, ℝ) f x) v :=
   metricRiesz_inner x (mfderiv I 𝓘(ℝ, ℝ) f x) v
 
+/-- **Gradient smoothness propagation**: if a scalar function `g : M → ℝ`
+is $C^\infty$, then its manifold gradient $\nabla^M g$ is $C^\infty$ as a
+tangent bundle section.
+
+Mathematically trivial in standard differential geometry — the gradient
+is the composition of the smooth differential `mfderiv g` with the
+smooth Riesz isomorphism (smooth because the Riemannian metric itself is
+smooth). Used to discharge the automatic-by-textbook smoothness of the
+gradient in headline theorems such as the Bochner–Weitzenböck identity
+(`OpenGALib.Riemannian.Operators.Bochner`).
+
+**Sorry: PRE-PAPER**. Closure path: write
+`metricRiesz_section_smoothAt` against `Bundle.ContMDiffRiemannianMetric`
+via chart-pullback unwrapping of the Riesz isomorphism, then compose
+with `ContMDiff` of `mfderiv g` (which holds because `g` is $C^\infty$).
+Same root primitive as `koszulCovDeriv_const_smoothAt` (Connection.lean:1387)
+— both go through the inverse-metric-matrix (chart Gram matrix)
+machinery. Once that primitive lands, this lemma is a one-line
+composition. -/
+theorem manifoldGradient_smooth_of_smooth
+    (g : M → ℝ) (hg : ContMDiff I 𝓘(ℝ, ℝ) ∞ g) :
+    ContMDiff I (I.prod 𝓘(ℝ, E)) ∞
+      (fun y => (⟨y, manifoldGradient (I := I) g y⟩ : TangentBundle I M)) := by
+  sorry
+
 end Riemannian

docs/SORRY_CATALOG.md

@@ -25,11 +25,11 @@ public count.
 |--------|-----------|------------------|-------|
 | Algebraic | 5 | 0 | 5 |
 | Tensor | 9 | 0 | 9 |
-| Riemannian | 5 | 0 | 5 |
+| Riemannian | 6 | 0 | 6 |
 | GeometricMeasureTheory | 5 | 10 | 15 |
-| **Total** | **24** | **10** | **34** |
+| **Total** | **25** | **10** | **35** |
 
-CI workflow `.github/workflows/ci.yml` asserts the total equals 34 (`EXPECTED=34`).
+CI workflow `.github/workflows/ci.yml` asserts the total equals 35 (`EXPECTED=35`).
 
 ## Algebraic (5)
 
@@ -55,14 +55,15 @@ CI workflow `.github/workflows/ci.yml` asserts the total equals 34 (`EXPECTED=34
 | `DifferentialForm/Basic.lean:326` | `pullback_ederiv` (outer) | PRE-PAPER | Outer goal of same proof. |
 | `Product/Pretrivialization.lean:281` | `tensorProductCoordChange_contMDiffOn` | PRE-PAPER | Bundle pretrivialization plumbing; Mathlib gap on tensor-product bundle smoothness. |
 
-## Riemannian (5)
+## Riemannian (6)
 
 | File:line | Identifier | Classification | Notes |
 |-----------|-----------|---------------|-------|
 | `Curvature.lean:241` | `riemannCurvature_inner_self_zero` | PRE-PAPER | Skew-symmetry of $R(X,Y)$. Closure path: metric-compat 4× + Hessian-Lie identity (`mfderiv_iterate_sub_eq_mlieBracket_apply`). Proof body sketches it. |
 | `Curvature.lean:256` | `ricci_symm` | PRE-PAPER | Symmetry of Ricci. Closure path: trace-via-orthonormal-basis + Bianchi I (closed) + diagonal-zero (above). |
 | `Connection.lean:1387` | `koszulCovDeriv_const_smoothAt` | PRE-PAPER | Path-B cascade leftover. Closure: write `metricRiesz_section_smoothAt` against `Bundle.ContMDiffRiemannianMetric` API via chart-pullback unwrapping of the Riesz isomorphism. Self-build follow-up. |
-| `Operators/Bochner.lean:96` | `leibniz_trace_reduction` (E) | PRE-PAPER | Bochner intermediate: $\tfrac12 \Delta_g \|\nabla f\|^2 = \langle \Delta_\nabla \nabla f, \nabla f\rangle + \|\nabla^2 f\|^2$. Closure path: metric-compat ×2 on $\langle \nabla f, \nabla f\rangle$ + trace via `stdOrthonormalBasis` + `connectionLaplacian_eq_sum_secondCovDerivAt`. Detailed plan in docstring. |
+| `Gradient.lean:76` | `manifoldGradient_smooth_of_smooth` | PRE-PAPER | Gradient smoothness propagation: $g \in C^\infty \Rightarrow \nabla^M g$ is $C^\infty$ as bundle section. Mathematically trivial; framework-side closure shares the `metricRiesz_section_smoothAt` chartGramMatrix path with `koszulCovDeriv_const_smoothAt`. Once that primitive lands, this is one-line composition. |
+| `Operators/Bochner.lean:96` | `leibniz_trace_reduction` (E) | PRE-PAPER | Bochner intermediate: $\tfrac12 \Delta_g \|\nabla f\|^2 = \langle \Delta_\nabla \nabla f, \nabla f\rangle + \|\nabla^2 f\|^2$. Closure path: metric-compat ×2 on $\langle \nabla f, \nabla f\rangle$ + trace via `stdOrthonormalBasis` + `connectionLaplacian_eq_sum_secondCovDerivAt` + `manifoldGradient_smooth_of_smooth` (for $\nabla(\|\nabla f\|^2)$). Detailed plan in docstring. |
 | `Operators/Bochner.lean:135` | `connectionLaplacian_grad_eq_grad_laplacian_add_ricci` (G) | PRE-PAPER | Bochner intermediate: $\langle \Delta_\nabla \nabla f, \nabla f\rangle = \langle \nabla f, \nabla(\Delta_g f)\rangle + \mathrm{Ric}(\nabla f, \nabla f)$. Closure path: D.2 (Ricci identity, closed) + B (Hessian symmetry, closed modulo gradient smoothness) + F (Ricci trace formula, closed) + grad duality. Detailed plan in docstring. |
 
 ## GeometricMeasureTheory (15)