Skip to content

Commit 06b5e29

Browse files
Xinze-Li-MoqianXinze-Li-Moqian
committed
Curvature: close ricci_symm via Bianchi-trace + diagonal-zero
Per-basis-vector Bianchi I on (const b_i, X, Y) plus first-pair antisymm collapses to R(const, X) Y - R(const, Y) X = -R(X, Y) (const). Tracing over stdOrthonormalBasis with LinearMap.trace_eq_sum_inner pairs each summand with -<R(X, Y)(const b_i), b_i> = 0 from inner_self_zero. Adds h_interior hypothesis (needed by inner_self_zero via Hessian-Lie). Net sorry -1: Curvature.lean now fully unconditional.
1 parent 96da01d commit 06b5e29

2 files changed

Lines changed: 147 additions & 13 deletions

File tree

‎OpenGALib/Riemannian/Curvature.lean‎

Lines changed: 146 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,9 @@ import OpenGALib.Riemannian.HessianLie
77
-- `import OpenGALib.Riemannian.Connection` above.
88
import Mathlib.LinearAlgebra.Trace
99
import Mathlib.Analysis.InnerProductSpace.PiL2
10+
import Mathlib.Analysis.InnerProductSpace.Trace
11+
import Mathlib.Geometry.Manifold.VectorField.LieBracket
12+
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
1013

1114
/-!
1215
# Riemann curvature, Ricci, and scalar curvature
@@ -36,14 +39,14 @@ and the metric-dependent Ricci / scalar-curvature constructions.
3639
## Main results
3740
3841
* `riemannCurvature_antisymm` — $R(X, Y) Z = -R(Y, X) Z$.
39-
* `riemannCurvature_inner_self_zero` (sorry, PRE-PAPER) — $\langle R(X, Y) Z, Z \rangle_g = 0$.
40-
* `ricci_symm` (sorry, PRE-PAPER) — $\mathrm{Ric}(X, Y) = \mathrm{Ric}(Y, X)$.
42+
* `riemannCurvature_inner_self_zero` — $\langle R(X, Y) Z, Z \rangle_g = 0$.
43+
* `ricci_symm` — $\mathrm{Ric}(X, Y) = \mathrm{Ric}(Y, X)$.
4144
4245
Reference: do Carmo 1992 §4.
4346
-/
4447

4548
open Bundle VectorField
46-
open scoped ContDiff Manifold Riemannian
49+
open scoped ContDiff Manifold Riemannian InnerProductSpace
4750

4851
namespace Riemannian
4952

@@ -591,20 +594,153 @@ theorem riemannCurvature_metric_skew
591594
-- h_ZW : g(R Z, Z) + g(R Z, W) + (g(R W, Z) + g(R W, W)) = 0
592595
linarith
593596

597+
/-! ### Constant-direction Bianchi swap
598+
599+
Specialisation of `bianchi_first` to the triple $(\mathrm{const}\,v, X, Y)$,
600+
combined with `riemannCurvature_antisymm` on the third Bianchi summand:
601+
$$R(\mathrm{const}\,v, X)\,Y - R(\mathrm{const}\,v, Y)\,X
602+
= -R(X, Y)(\mathrm{const}\,v).$$
603+
This is the per-basis-vector algebraic identity that drives `ricci_symm`. -/
604+
605+
/-- **Constant-direction Bianchi swap**. Bianchi I on $(\mathrm{const}\,v, X, Y)$
606+
together with first-pair antisymmetry of $R$ rearranges to the form needed
607+
for the Ricci-symmetry trace argument. -/
608+
private lemma riemannCurvature_const_first_swap_eq_neg
609+
[IsManifold I 2 M]
610+
(v : E) (X Y : SmoothVectorField I M) (x : M) :
611+
riemannCurvature (fun _ : M => v) X.toFun Y.toFun x
612+
- riemannCurvature (fun _ : M => v) Y.toFun X.toFun x
613+
= -riemannCurvature X.toFun Y.toFun (fun _ : M => v) x := by
614+
classical
615+
set V : SmoothVectorField I M := SmoothVectorField.const (I := I) (M := M) v with hV_def
616+
-- Pointwise smoothness witnesses for V, X, Y.
617+
have hV_smooth : ∀ y, TangentSmoothAt (fun _ : M => v) y := V.smoothAt
618+
have hX_smooth : ∀ y, TangentSmoothAt X.toFun y := X.smoothAt
619+
have hY_smooth : ∀ y, TangentSmoothAt Y.toFun y := Y.smoothAt
620+
-- First-derivative sections smooth.
621+
have h_dVY : ∀ y, TangentSmoothAt
622+
(fun y' => covDeriv (fun _ : M => v) Y.toFun y') y :=
623+
fun y => covDeriv_const_smoothVF_smoothAt v Y y
624+
have h_dXV : ∀ y, TangentSmoothAt
625+
(fun y' => covDeriv X.toFun (fun _ : M => v) y') y :=
626+
fun y => covDeriv_smoothVF_smoothAt X V y
627+
have h_dYX : ∀ y, TangentSmoothAt
628+
(fun y' => covDeriv Y.toFun X.toFun y') y :=
629+
fun y => covDeriv_smoothVF_smoothAt Y X y
630+
-- Lie-bracket sections smooth.
631+
have h_VX_br : ∀ y, TangentSmoothAt
632+
(fun y' => mlieBracket I (fun _ : M => v) X.toFun y') y :=
633+
fun y => mlieBracket_tangentSmoothAt V.smooth X.smooth
634+
have h_XV_br : ∀ y, TangentSmoothAt
635+
(fun y' => mlieBracket I X.toFun (fun _ : M => v) y') y :=
636+
fun y => mlieBracket_tangentSmoothAt X.smooth V.smooth
637+
have h_XY_br : ∀ y, TangentSmoothAt
638+
(fun y' => mlieBracket I X.toFun Y.toFun y') y :=
639+
fun y => mlieBracket_tangentSmoothAt X.smooth Y.smooth
640+
have h_YV_br : ∀ y, TangentSmoothAt
641+
(fun y' => mlieBracket I Y.toFun (fun _ : M => v) y') y :=
642+
fun y => mlieBracket_tangentSmoothAt Y.smooth V.smooth
643+
have h_VY_br : ∀ y, TangentSmoothAt
644+
(fun y' => mlieBracket I (fun _ : M => v) Y.toFun y') y :=
645+
fun y => mlieBracket_tangentSmoothAt V.smooth Y.smooth
646+
-- Jacobi identity at x from Mathlib (`leibniz_identity_mlieBracket_apply`).
647+
-- Smoothness witnesses at level `minSmoothness ℝ 2`, downgraded from ∞.
648+
have hV_2 : ContMDiffAt I (I.prod 𝓘(ℝ, E)) (minSmoothness ℝ 2)
649+
(fun y => (⟨y, (fun _ : M => v) y⟩ : TangentBundle I M)) x := by
650+
rw [minSmoothness_of_isRCLikeNormedField]
651+
exact (V.smooth x).of_le (by
652+
show ((2 : ℕ∞) : ℕ∞ω) ≤ ∞
653+
exact_mod_cast (le_top : (2 : ℕ∞) ≤ ⊤))
654+
have hX_2 : ContMDiffAt I (I.prod 𝓘(ℝ, E)) (minSmoothness ℝ 2)
655+
(fun y => (⟨y, X.toFun y⟩ : TangentBundle I M)) x := by
656+
rw [minSmoothness_of_isRCLikeNormedField]
657+
exact (X.smooth x).of_le (by
658+
show ((2 : ℕ∞) : ℕ∞ω) ≤ ∞
659+
exact_mod_cast (le_top : (2 : ℕ∞) ≤ ⊤))
660+
have hY_2 : ContMDiffAt I (I.prod 𝓘(ℝ, E)) (minSmoothness ℝ 2)
661+
(fun y => (⟨y, Y.toFun y⟩ : TangentBundle I M)) x := by
662+
rw [minSmoothness_of_isRCLikeNormedField]
663+
exact (Y.smooth x).of_le (by
664+
show ((2 : ℕ∞) : ℕ∞ω) ≤ ∞
665+
exact_mod_cast (le_top : (2 : ℕ∞) ≤ ⊤))
666+
-- `leibniz_identity_mlieBracket_apply` needs `IsManifold I (minSmoothness ℝ 3) M`;
667+
-- provide it from `IsManifold I ∞ M` (`LEInfty` cascade on `ℕ∞ω`).
668+
haveI hM3 : IsManifold I (minSmoothness ℝ 3) M := by
669+
rw [minSmoothness_of_isRCLikeNormedField]; infer_instance
670+
have h_jac := VectorField.leibniz_identity_mlieBracket_apply
671+
(I := I) (M := M) (U := fun _ : M => v) (V := X.toFun) (W := Y.toFun)
672+
hV_2 hX_2 hY_2
673+
-- Bianchi I with (X', Y', Z') = (const v, X.toFun, Y.toFun).
674+
have h_bianchi := bianchi_first (fun _ : M => v) X.toFun Y.toFun x
675+
hV_smooth hX_smooth hY_smooth
676+
h_dVY h_dXV h_dYX
677+
h_VX_br h_XV_br h_XY_br h_YV_br h_VY_br
678+
h_jac
679+
-- First-pair antisymmetry on the 3rd Bianchi summand.
680+
have h_antisym :
681+
riemannCurvature Y.toFun (fun _ : M => v) X.toFun x
682+
= -riemannCurvature (fun _ : M => v) Y.toFun X.toFun x :=
683+
riemannCurvature_antisymm Y.toFun (fun _ : M => v) X.toFun x
684+
rw [h_antisym] at h_bianchi
685+
-- h_bianchi : R(V,X) Y + R(X,Y) V + - R(V,Y) X = 0
686+
-- Goal: R(V,X) Y - R(V,Y) X = -R(X,Y) V ⇔ (R(V,X) Y - R(V,Y) X) + R(X,Y) V = 0.
687+
apply eq_neg_of_add_eq_zero_left
688+
-- Rearrange h_bianchi via `abel`.
689+
rw [show (riemannCurvature (fun _ : M => v) X.toFun Y.toFun x
690+
- riemannCurvature (fun _ : M => v) Y.toFun X.toFun x
691+
+ riemannCurvature X.toFun Y.toFun (fun _ : M => v) x
692+
: TangentSpace I x)
693+
= riemannCurvature (fun _ : M => v) X.toFun Y.toFun x
694+
+ riemannCurvature X.toFun Y.toFun (fun _ : M => v) x
695+
+ -riemannCurvature (fun _ : M => v) Y.toFun X.toFun x from by abel]
696+
exact h_bianchi
697+
594698
/-- $\mathrm{Ric}(X, Y) = \mathrm{Ric}(Y, X)$.
595699
596700
Reference: do Carmo §4 ex. 1.
597701
598-
**Sorry: PRE-PAPER**. Closure path: trace-via-orthonormal-basis + Bianchi I +
599-
first-arg antisymmetry of $R$ + diagonal-zero (`riemannCurvature_inner_self_zero`).
600-
For each $e_i$ in an orthonormal basis, Bianchi I on $(\mathrm{const}\,e_i, X, Y)$
601-
gives $\langle R(e_i, X) Y, e_i\rangle - \langle R(e_i, Y) X, e_i\rangle = -\langle R(X, Y) e_i, e_i\rangle$;
602-
summing produces $\mathrm{Ric}(X, Y) - \mathrm{Ric}(Y, X) = -\mathrm{tr}(R(X, Y)) = 0$. -/
702+
Closure via:
703+
* `LinearMap.trace_eq_sum_inner` on `curvatureEndo X Y x` against
704+
`stdOrthonormalBasis ℝ (T_xM)` (so each Ricci scalar is a sum of
705+
$\langle b_i, R(\mathrm{const}\,b_i, X)\,Y\,x\rangle$ pairings),
706+
* `riemannCurvature_const_first_swap_eq_neg` per basis vector (Bianchi I +
707+
antisym packaging),
708+
* `riemannCurvature_inner_self_zero` on $(X, Y, \mathrm{const}\,b_i)$ to kill
709+
every summand.
710+
711+
The hypothesis `h_interior` is required by `riemannCurvature_inner_self_zero`
712+
(via the Hessian-Lie identity on boundary-aware models). -/
603713
theorem ricci_symm
604714
[IsManifold I 2 M]
605-
(X Y : SmoothVectorField I M) (x : M) :
715+
(X Y : SmoothVectorField I M) (x : M)
716+
(h_interior : extChartAt I x x ∈ closure (interior (Set.range I))) :
606717
Ric(X, Y) x = Ric(Y, X) x := by
607-
sorry
718+
classical
719+
set b := stdOrthonormalBasis ℝ (TangentSpace I x) with hb_def
720+
-- Expand each Ricci scalar as `∑ i, ⟪b i, R(const b i, ·) · x⟫_ℝ` via
721+
-- `LinearMap.trace_eq_sum_inner`.
722+
have h_RXY : Ric(X, Y) x =
723+
∑ i, ⟪b i, riemannCurvature (fun _ : M => (b i : E)) X.toFun Y.toFun x⟫_ℝ := by
724+
show LinearMap.trace ℝ (TangentSpace I x) (curvatureEndo X Y x) = _
725+
exact LinearMap.trace_eq_sum_inner _ b
726+
have h_RYX : Ric(Y, X) x =
727+
∑ i, ⟪b i, riemannCurvature (fun _ : M => (b i : E)) Y.toFun X.toFun x⟫_ℝ := by
728+
show LinearMap.trace ℝ (TangentSpace I x) (curvatureEndo Y X x) = _
729+
exact LinearMap.trace_eq_sum_inner _ b
730+
rw [h_RXY, h_RYX]
731+
-- Per i: the two inner products are equal (their difference vanishes
732+
-- by const-swap Bianchi + diagonal-zero).
733+
refine Finset.sum_congr rfl (fun i _ => ?_)
734+
rw [← sub_eq_zero, ← inner_sub_right,
735+
riemannCurvature_const_first_swap_eq_neg (I := I) (M := M) (b i : E) X Y x]
736+
-- Goal: ⟪b i, -R(X, Y) (const b i) x⟫_ℝ = 0
737+
rw [inner_neg_right, neg_eq_zero]
738+
-- Goal: ⟪b i, R(X, Y) (const b i) x⟫_ℝ = 0
739+
-- Use real_inner_comm + riemannCurvature_inner_self_zero (with Z = cF[b i]).
740+
rw [real_inner_comm]
741+
-- Goal: ⟪R(X, Y) (const b i) x, b i⟫_ℝ = 0 (def-eq metricInner via hm.metric).
742+
exact riemannCurvature_inner_self_zero X Y
743+
(SmoothVectorField.const (I := I) (M := M) (b i : E)) x h_interior
608744

609745
/-- The **Ricci tensor** at $x$ as a bilinear form $T_xM \times T_xM \to \mathbb{R}$,
610746
$(V, W) \mapsto \mathrm{Ric}(V, W)(x)$ with $V, W$ extended to constant sections.

‎docs/SORRY_CATALOG.md‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -55,12 +55,10 @@ CI workflow `.github/workflows/ci.yml` asserts the total equals 34 (`EXPECTED=34
5555
| `DifferentialForm/Basic.lean:326` | `pullback_ederiv` (outer) | PRE-PAPER | Outer goal of same proof. |
5656
| `Product/Pretrivialization.lean:281` | `tensorProductCoordChange_contMDiffOn` | PRE-PAPER | Bundle pretrivialization plumbing; Mathlib gap on tensor-product bundle smoothness. |
5757

58-
## Riemannian (5)
58+
## Riemannian (3)
5959

6060
| File:line | Identifier | Classification | Notes |
6161
|-----------|-----------|---------------|-------|
62-
| `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. |
63-
| `Curvature.lean:256` | `ricci_symm` | PRE-PAPER | Symmetry of Ricci. Closure path: trace-via-orthonormal-basis + Bianchi I (closed) + diagonal-zero (above). |
6462
| `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. |
6563
| `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. |
6664
| `Operators/Bochner.lean` | `sum_inner_secondCovDerivAt_grad_eq_inner_grad_laplacian_add_ricci` (G inner) | PRE-PAPER | Bochner heart-of-Bochner sum identity (focused private helper used by G): $\sum_i \langle (\nabla^2 \nabla f)(\varepsilon_i, \varepsilon_i), \nabla f\rangle_g = \langle \nabla f, \nabla(\Delta_g f)\rangle_g + \mathrm{Ric}(\nabla f, \nabla f)$. The full G theorem (`connectionLaplacian_grad_eq_grad_laplacian_add_ricci`) is proved modulo this sum identity. **Steps 1-3 closed via D.3** (`secondCovDerivSection_sub_swap_eq_riemannCurvature` in `Operators/ConnectionLaplacian.lean`) + Hess sym (B) + Ricci tensor identification (F). **Step 4 (∇Δf identification) blocked**: chart-frame constant lift $\tilde\varepsilon_i$ is not $g$-orthonormal off $x$, so $\sum_i \mathrm{Hess}\,f(y)(\varepsilon_i,\varepsilon_i) \ne \Delta_g f(y)$ for $y \ne x$, breaking the gradient-direction trace identification. **Repair**: port `external/differential-geometry/.../RicciIdentitySmoothFrame.lean` `smoothOrthoFrame g x` (chart-bump × Gram-Schmidt; ~500-1000 LOC). **Repair owner**: framework self-build (next session). |

0 commit comments

Comments
 (0)