Refactor Riemannian Util layout and simp helpers (#5 #6 #7)#41

Closed

poet77 wants to merge 35 commits into

killing-pdefrom

Commits on May 15, 2026

initial commit
Xinze-Li-Moqian
committed

Commits on May 17, 2026

Killing field PDE: full proof (∇²_{Y,Z} X = R(Y, X) Z)

zhifeizhu92
authored and
Xinze-Li-Moqian
committed
Volume Phase 1a: gramMatrix + sqrtGramDet (Util/GramDeterminant)
Xinze-Li-Moqian
committed
Volume Phase 1d-ii: chartSqrtGramDet + bridge to abstract sqrtGramDet
Xinze-Li-Moqian
committed
Volume Phase 1d-iii: chart-transition matrix + Gram pullback
Xinze-Li-Moqian
committed
Volume Phase 1d-iv-a: chartLocalMeasure construction (ChartDensity equivalent)
Xinze-Li-Moqian
committed
Volume Phase 1d-iv-b: chart-overlap geometric plumbing (ChartOverlap)
Xinze-Li-Moqian
committed
Volume Phase 1d-iv-c: ChartLocalIntegral (B3 batch 2)
Xinze-Li-Moqian
committed
Volume Phase 1d-iv-d: chartAtlasPOU + riemannianMeasure (Glue)
Xinze-Li-Moqian
committed
Volume Phase 1 facade: ChartPullback (volumeMeasure + locally-finite)
Xinze-Li-Moqian
committed
Volume Phase 2 skeleton: VolumeForm (pointwise volume form dV_g(x))
Xinze-Li-Moqian
committed
Volume Phase 3: Hausdorff bridge (Federer constant + vol_g = α(n)·μH[n])
Xinze-Li-Moqian
committed
Volume Phase 4 placeholder: Exponential.lean (Mathlib gap doc)
Xinze-Li-Moqian
committed
Volume Phase 5 skeleton: UniversalProperty (volumeMeasure_unique)
Xinze-Li-Moqian
committed
BG: tighten signature to vol_g + retire IsScalarMultipleOfHausdorff stopgap
Xinze-Li-Moqian
committed
ci: bump EXPECTED_SHAKE 35 → 36 for Volume/Util/GramDeterminant
Xinze-Li-Moqian
committed
Merge pull request #30 from MathNetwork/riemannian-volume
Xinze-Li-Moqian
authored
Curvature 9a (Phase 1): explicit g on Ricci/scalarCurvature core
Xinze-Li-Moqian
committed
Merge pull request #31 from MathNetwork/refactor/explicit-g-9a
Xinze-Li-Moqian
authored

Commits on May 18, 2026