9f: explicit-g cascade — Tensoriality/RiemannCurvature/bianchi_first + Bochner wrappers#38
Merged
Merged
Conversation
Lifts the explicit-g cascade through: - Util/MetricInnerSmoothness: add Riemannian.RiemannianMetric.metricInner_mdifferentiableAt_of_tangentSmoothAt (explicit-g variant of typeclass helper) - Operators/Bochner/HessianExpansion: full lift to (g : RiemannianMetric I M) section variable; body uses g.metricInner, manifoldGradient g, etc.; ‖grad_g[I] f‖²_g notation expanded inline - Curvature/Tensoriality: full mass lift with include g; all riemannCurvature_eq_of_X/Y/Z_eq_at, _pointwise_eq, add_first, smul_third/first, eventuallyEq, zero_of_zero theorems now take explicit g; local g shadowing fixed via rename to c - Curvature/RiemannCurvature: riemannCurvature_antisymm, riemannCurvature_add_third lifted to explicit g; internal callers updated Consumer fixups: - Operators/Bochner: pass HasMetric.metric to hessian_gradientNormSq_apply_section; add show cast to bridge ‖V‖²_g notation - Operators/Bochner/BochnerExpansion: pass HasMetric.metric to riemannCurvature_eq_of_pointwise_eq Defers to follow-up: - BochnerExpansion/PerSummand/Bochner.lean full body lift requires lifting ricci_symm, riemannCurvature_inner_self_zero, bianchi_first, SmoothOrthoFrame wrappers (cascade depth ~10+ theorems); separate PR. - Notation drop and metricInner typeclass abbrev deletion deferred.
Continues the upstream cascade started in Phase 1: - LeviCivita.bianchi_first lifted; ∇[X] Y / ⟦X, Y⟧ notations expanded inline in body - RiemannCurvature.mDirDeriv_self_eq_two_metricInner_leviCivita_self lifted - RiemannCurvature.fun_mDirDeriv_self_eq_two_metricInner_leviCivita_self lifted - RiemannCurvature.half_mDirDeriv_iterate_eq_metricInner_iterCovDeriv lifted - RiemannCurvature.riemannCurvature_inner_self_zero lifted (statement: g.metricInner ... = 0; body uses Riem notation in some places — kept where downstream typeclass-form needed) - RiemannCurvature.riemannCurvature_const_first_swap_eq_neg lifted (uses lifted bianchi_first + antisymm) ricci_symm intentionally NOT lifted: its proof routes through ⟪·,·⟫_ℝ (= hm.metric.inner via InnerProductSpace instance), so lifting requires either g = hm.metric hypothesis or instance restructuring. Consumers (Bochner) call ricci_symm with implicit typeclass form; works under typical use where g = hm.metric. riemannCurvature_metric_skew internal callers pass HasMetric.metric to lifted riemannCurvature_inner_self_zero.
- ricci_symm statement: Ric(X, Y) notation → explicit ricci HasMetric.metric form (kept typeclass since proof routes through ⟪·,·⟫_ℝ = hm.metric.inner via InnerProductSpace instance — lifting to arbitrary g requires either g = hm.metric hypothesis or trace-without-inner-product refactor) - BochnerExpansion: riemannCurvature_eq_of_pointwise_eq caller updated to pass HasMetric.metric (matches Tensoriality lift)
Adds explicit-g wrappers for the three public-facing Bochner theorems via subst hg pattern: - bochner_leibniz_trace_reduction_g (Operators/Bochner.lean) - bochner_connectionLaplacian_grad_decomposition_g (Operators/Bochner/PerSummand.lean) - bochner_weitzenboeck_g (Operators/Bochner.lean) Each wrapper takes (g : RiemannianMetric I M) (hg : g = hm.metric) and discharges via subst hg + typeclass version. Provides explicit-g API surface without requiring lift of internal proof bodies (which depend on ricci_symm + smoothOrthoFrame chain still tied to ⟪·,·⟫_ℝ = hm.metric.inner via InnerProductSpace instance). End users pass hm.metric for g and rfl for hg to consume.
This was referenced May 18, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
9f sub-task of umbrella #9 (explicit-g cascade). Lifts upstream curvature/connection theorems and provides explicit-g headline wrappers for the Bochner stack. 4 phases, full build green.
Phase 1 (3b7ab95) — HessianExpansion + Tensoriality + 2 RiemannCurvature
Util/MetricInnerSmoothness.lean: add explicit-gmetricInner_mdifferentiableAt_of_tangentSmoothAtinRiemannian.RiemannianMetricnamespaceOperators/Bochner/HessianExpansion.lean: full lift to(g : RiemannianMetric I M)section variable; body usesg.metricInner,manifoldGradient g, etc.;‖grad_g[I] f‖²_gnotation expanded inlineCurvature/Tensoriality.lean: full mass lift withinclude g(12 theorems); localgshadow renamed tocCurvature/RiemannCurvature.lean:riemannCurvature_antisymm,riemannCurvature_add_thirdlifted; internal callers passHasMetric.metricfor downstream typeclass pathsPhase 2 (33e7c12) — bianchi_first + curvature self-zero chain
Connection/LeviCivita.lean:bianchi_firstlifted;∇[...]/⟦·,·⟧notations expandedCurvature/RiemannCurvature.lean: 5 more theorems lifted (mDirDeriv_self_eq_two_metricInner_leviCivita_self,fun_*,half_mDirDeriv_iterate_*,riemannCurvature_inner_self_zero,riemannCurvature_const_first_swap_eq_neg)Phase 3 (73922df) —
ricci_symmstatement explicit + Bochner callerricci_symmstatement converted fromRic(X, Y)notation to explicitricci HasMetric.metricform (kept typeclass since proof routes through⟪·,·⟫_ℝ = hm.metric.innervia InnerProductSpace instance — full lift requires eitherg = hm.metrichypothesis or trace-without-inner refactor)BochnerExpansion:riemannCurvature_eq_of_pointwise_eqcaller updated to passHasMetric.metric(matches Tensoriality lift)Phase 4 (9dd2383) — explicit-g wrappers for Bochner headlines
Adds three explicit-g wrappers via
subst hgpattern:bochner_leibniz_trace_reduction_gbochner_connectionLaplacian_grad_decomposition_gbochner_weitzenboeck_gEach takes
(g : RiemannianMetric I M) (hg : g = hm.metric)and discharges viasubst hg+ typeclass version. End users call asbochner_weitzenboeck_g hm.metric rfl f hf x.Stats
8 files, +832 / -762 lines, ~20 upstream theorems lifted in place, 3 explicit-g wrappers added.
Deferred (separate PR)
Internal Bochner stack body lift (
BochnerExpansion.lean/PerSummand.lean/bochner_leibniz_trace_reductionbody) requires liftingricci_symm+ SmoothOrthoFrame wrappers, which depend on⟪·,·⟫_ℝ(InnerProductSpaceinstance fromhm.metric). Two paths:(hg : g = hm.metric)hypothesis throughout (uniform but invasive)LinearMap.trace_eq_sum_inner(deeper refactor)For now, public API is g-parametric through the Phase 4 wrappers; internal proofs stay typeclass-bound.
Test plan
lake buildclean (3668 jobs)