9i: lift Bochner stack (BochnerExpansion + PerSummand) to explicit g via subst hg#44

Merged

Xinze-Li-Moqian merged 6 commits into

mainfrom

refactor/explicit-g-9i

May 18, 2026

Commits on May 18, 2026

9h: lift riemannCurvature_metric_skew / _pair_symm / sectionalCurvature(At) / _symmetric to explicit g
Xinze-Li-Moqian
committed
9h: lift IsFlat predicate to explicit g (IsKilling kept typeclass — deep proof cascade)
Xinze-Li-Moqian
committed
9h: lift IsKilling + second_covDeriv_(inner_skew|commutator|eq_curvature) to explicit g
Xinze-Li-Moqian
committed
9h: lift ricci_symm to explicit g via (hg : g = hm.metric) hypothesis
Xinze-Li-Moqian
committed
9i: lift BochnerExpansion.lean to explicit g (via subst hg pattern)
Xinze-Li-Moqian
committed
9i: lift PerSummand.lean to explicit g (via subst hg pattern)
Xinze-Li-Moqian
committed