Thanks for 38adeaf killing equ fix. The proof part has been partially merged into main (commit 662b86d). Below is the feedback and the adjustments you'll need to make.
✅ Merged
The whole new block in OpenGALib/Riemannian/Curvature/RiemannCurvature.lean:
private lemma IsKilling.second_covDeriv_inner_skewprivate lemma second_covDeriv_commutatortheorem IsKilling.second_covDeriv_eq_curvature (full proof)
Full lake build passes; sorry / shake baselines unchanged. The RHS sign correction Riem(X, Y) Z → Riem(Y, X) Z is preserved — it matches OpenGA's commutator-form convention Riem(U,V) = ∇_U∇_V − ∇_V∇_U − ∇_[U,V].
No code-quality issues to address: Math tags in place, the two private helpers in the anchor file fall under the documented exemption, signature reads cleanly, no maxHeartbeats hacks. The convention compliance is clean.
⚠️ Not merged
These two fixes from your commit had no target file on main and were dropped:
OpenGALib/Riemannian/Volume/Hausdorff.lean — explicit definition of alphaFedererConstantOpenGALib/Riemannian/Volume/ChartPullback.lean — instSigmaFinite switched to infer_instance
main currently has no Riemannian/Volume/ directory at all.
🔀 Branch state
I recently did a large refactor + squash-rebase on main, so mathnetwork/main and mathnetwork/killing-pde are now two histories with no common ancestor (git merge-base returns empty). CI baselines also diverged:
| Metric |
main |
killing-pde |
| Sorry count (tightened regex) |
32 |
36 |
| Shake suggestions |
35 |
39 |
📋 Action items
Thanks for
38adeaf killing equ fix. The proof part has been partially merged intomain(commit 662b86d). Below is the feedback and the adjustments you'll need to make.✅ Merged
The whole new block in
OpenGALib/Riemannian/Curvature/RiemannCurvature.lean:private lemma IsKilling.second_covDeriv_inner_skewprivate lemma second_covDeriv_commutatortheorem IsKilling.second_covDeriv_eq_curvature(full proof)Full
lake buildpasses; sorry / shake baselines unchanged. The RHS sign correctionRiem(X, Y) Z → Riem(Y, X) Zis preserved — it matches OpenGA's commutator-form conventionRiem(U,V) = ∇_U∇_V − ∇_V∇_U − ∇_[U,V].No code-quality issues to address: Math tags in place, the two
privatehelpers in the anchor file fall under the documented exemption, signature reads cleanly, nomaxHeartbeatshacks. The convention compliance is clean.These two fixes from your commit had no target file on
mainand were dropped:OpenGALib/Riemannian/Volume/Hausdorff.lean— explicit definition ofalphaFedererConstantOpenGALib/Riemannian/Volume/ChartPullback.lean—instSigmaFiniteswitched toinfer_instancemaincurrently has noRiemannian/Volume/directory at all.🔀 Branch state
I recently did a large refactor + squash-rebase on
main, somathnetwork/mainandmathnetwork/killing-pdeare now two histories with no common ancestor (git merge-basereturns empty). CI baselines also diverged:📋 Action items
killing-pdebranch; cut new working branches frommathnetwork/mainVolume/fixes: first rungrep -r "alphaFedererConstant\|SigmaFinite.*volumeMeasure" OpenGALibonmainto see whether these concepts were refactored elsewhere, then decide whether to redo themmaindirectly; commit-message style can stay as before