Killing PDE merge: feedback & branch sync needed

[Xinze-Li-Moqian]

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_skew
• private lemma second_covDeriv_commutator
• theorem 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 alphaFedererConstant
• OpenGALib/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

• Retire your local killing-pde branch; cut new working branches from mathnetwork/main
• Stash or patch-save any uncommitted local work before switching
• For the Volume/ fixes: first run grep -r "alphaFedererConstant\|SigmaFinite.*volumeMeasure" OpenGALib on main to see whether these concepts were refactored elsewhere, then decide whether to redo them
• Future PRs: branch off the new main directly; commit-message style can stay as before

[Xinze-Li-Moqian]

killing-pde → main rebase: API impact checklist

Since this issue was opened, the explicit-g cascade (umbrella #9, now closed) landed in full on main. killing-pde is currently 15+ commits behind. When you rebase, here are the API changes to expect, ranked by likely impact on the killing-pde work:

1. All Riemannian-stack theorems now take explicit (g : RiemannianMetric I M)

Anywhere killing-pde calls these, you'll need to prepend g (and often an (hg : g = hm.metric) witness):

• Bochner anchors: bochner_weitzenboeck, bochner_leibniz_trace_reduction, bochner_connectionLaplacian_grad_decomposition
• Curvature: ricci_symm, bianchi_first, riemannCurvature, ricciTensor, scalarCurvature
• Operators: connectionLaplacian, scalarLaplacian, manifoldGradient, hessian, hessianBilin, divergence, secondFundamentalForm
• GMT consumers: firstVariationFull, secondVariationFull

Pattern when proving against a typeclass-bound metric: declare (g, hg) + include g hg, then subst hg at proof start.

2. metricInner typeclass abbrev deleted (9j, #45)

metricInner x v w no longer dispatches via typeclass. Use g.metricInner x v w (or hm.metric.metricInner x v w if still typeclass-bound). Wrapper functions also removed: metricToDual, metricRiesz, metricToDualEquiv — call the corresponding methods directly on the metric.

3. 13 _g polymorphic notations deleted (9g, #39/#40)

All gone: ⟪·,·⟫_g, ‖·‖²_g, Ric_g, scal_g[I], H_g[I], grad_g[I] f, Δ_g[I] f, hess_g[I] f, K_g[I](X,Y), Riem(X,Y)Z, II(X,Y), (∇R)[X](Y,Z)W. Replace with long-form names (g.metricInner, ricci g X Y x, scalarCurvature g x, hessian g f X Y x, etc.).

4. connectionLaplacian body uses smoothOrthoFrame g (9k, #47)

Was smoothOrthoFrame hm.metric. If killing-pde does unfold connectionLaplacian then hand-tackles the resulting sum, the orthoframe spelling has changed. The connectionLaplacian_def simp lemma RHS also updated. Mechanical fix.

5. CI baseline changes

• EXPECTED_SHAKE: 39 → 38 (9j removed ~180 LOC and dropped 1 unused import along the way). Bump down or remove unused imports during rebase.
• EXPECTED_ANCHOR_PURITY, EXPECTED_MATH_TAG, EXPECTED_NAMING: all 0. New files added in killing-pde may trip these — run linters during rebase.
• CI workflow (ci: incremental build on PRs — drop forced fresh elaboration (6m → 30s) #46): forced fresh elaboration dropped on PRs; incremental build only. full-lint-on-main is the new safety net (main push only, fresh elaboration). PR feedback should be much faster (~1-2 min instead of 6).

6. Expected textual conflicts with killing-pde's own work

These are the hot files where killing-pde's existing commits and main's cascade both touched the same regions:

• OpenGALib/Riemannian/Manifold/SmoothManifold.lean — 9j (9j: delete metricInner typeclass abbrev — end of typeclass-bound metric API #45) deleted ~180 LOC (MetricAPI section: metricInner abbrev + 14 wrapper lemmas); killing-pde's RiemannianMetric anchor refactor: split type/class out, move Eng to Util is in the same neighborhood. Will need manual reconciliation.
• OpenGALib/Riemannian/Metric/RiemannianMetric.lean — same story.
• OpenGALib/Riemannian/Operators/Bochner.lean and Bochner/{BochnerExpansion,PerSummand,HessianExpansion}.lean — 9f/9i/9k touched extensively; killing-pde's bochner-area edits will need rebasing.
• OpenGALib/Comparison/BishopGromov/VolumeComparison.lean — 9e (Consumers 9e: explicit g on BG / Variation / Stationary / Stable #37) made it explicit-g; killing-pde's BG signature refactor (drop IsScalarMultipleOfHausdorff stopgap) is in the same surface.
• OpenGALib/Riemannian/Connection/LeviCivita.lean — 9b/9c/9f all touched.

Reference: cascade PRs

In chronological merge order on main: #30, #31, #33, #34, #35, #36, #37, #38, #39, #40, #42, #44, #45, #46, #47. Each PR description includes the per-file refactor pattern (subst hg insertion, etc.) which should help apply the same pattern to killing-pde code.

Happy to help with any specific file if rebase friction shows up — ping here or open a fresh issue.

[Xinze-Li-Moqian]

@zhifeizhu92 — got the verification from your side (relayed to me; sounds like your AI session hit the 403 Resource not accessible by integration wall when trying to post directly).

Confirmed: retire killing-pde locally, go ahead.

Quick summary of the state as I have it on this end:

• mathnetwork/main has all the killing-pde-unique work already (the Killing PDE theorem with Riem(Y, X) Z, alphaFedererConstant, instSigmaFinite_volumeMeasure via infer_instance, Volume/ directory in full).
• mathnetwork/main and mathnetwork/killing-pde have no common ancestor — the squash-rebase severed the relationship. A git rebase killing-pde origin/main would produce a meaningless diff, so retiring the local branch is the correct move (not a rebase).
• No outstanding PR or patch is expected from killing-pde; nothing to port over.

Action for you:

git fetch mathnetwork
git checkout main
git reset --hard mathnetwork/main
git branch -D killing-pde       # optional, after confirming nothing local you need

Future branches: cut from mathnetwork/main directly. If you have uncommitted local work on killing-pde, git stash first or save as a patch (git diff > /tmp/killing-pde-local.patch) so you can replay selectively against main.

Re the comment-from-AI integration error: that's a GitHub-side ACL — write role's token can usually post comments on issues you didn't open, but actions integration may be scoped tighter. If it keeps blocking you, I (admin) or @poet77 (maintain) can post on your behalf — just ping us.

Closing this issue once you confirm the retire is done on your side. The follow-up engineering work is now tracked under the post-cascade umbrella #48 + sub-issues #49–#56, all assigned with split-as-you-see-fit guidance.