Search results

Killing PDE merge: feedback & branch sync needed

Status: Open.

#29 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 17, 2026

Prove IsKilling.length_sq_directional_eq_zero (Killing fields have constant length along their own flow)

mathMathematical content / proof workMathematical content / proof work

Status: Open.

#25 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

Prove IsKilling.divergence_eq_zero (Killing fields are divergence-free)

mathMathematical content / proof workMathematical content / proof work

Status: Open.

#24 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

Prove scalarLaplacian_mul (Laplace–Beltrami product rule)

mathMathematical content / proof workMathematical content / proof work

Status: Open.

#23 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

[9f] Explicit-g: Drop typeclass-dispatch _g notations entirely

architectureDesign / module organization changesDesign / module organization changes

refactorCode restructuring / reorganizationCode restructuring / reorganization

Status: Open.

#19 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

[9d] Explicit-g: Bochner stack internals

architectureDesign / module organization changesDesign / module organization changes

mathMathematical content / proof workMathematical content / proof work

refactorCode restructuring / reorganizationCode restructuring / reorganization

Status: Open.

#17 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

[Umbrella] Engineering hygiene sweep — Util layout + tech debt cleanup

architectureDesign / module organization changesDesign / module organization changes

refactorCode restructuring / reorganizationCode restructuring / reorganization

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#13 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

Prove bianchi_second (differential Bianchi identity)

mathMathematical content / proof workMathematical content / proof work

Status: Open.

#12 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

[Umbrella] Explicit-g cascade: drop [HasMetric I M] auto-resolution from Riemannian stack

architectureDesign / module organization changesDesign / module organization changes

mathMathematical content / proof workMathematical content / proof work

refactorCode restructuring / reorganizationCode restructuring / reorganization

Status: Open.

#9 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

Eliminate set_option backward.isDefEq.respectTransparency false workarounds

blocked-upstreamWaiting on Mathlib / Lean upstreamWaiting on Mathlib / Lean upstream

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#8 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

Rename ChartJacobianSmooth / ChartJacobianSmoothness for clarity

namingIdentifier / file naming cleanupIdentifier / file naming cleanup

refactorCode restructuring / reorganizationCode restructuring / reorganization

Status: Open.

#7 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026

Merge small Util files: OperatorSimp + CovDeriv consolidation

refactorCode restructuring / reorganizationCode restructuring / reorganization

tech-debtKnown engineering debt to clean upKnown engineering debt to clean up

Status: Open.

#6 In MathNetwork/OpenGA;

· Xinze-Li-Moqian opened on May 15, 2026