4 Ricci flow on left-invariant metrics
This branch is closed end to end. It is the one part of the road with no PDE in it, and everything below is proved: no sorry, no proof_wanted, all axiom-free.
A left-invariant metric on a Lie group \(G\) is determined by an inner product on \(\mathfrak {g}\), so \(\partial _t g= -2\operatorname {Ric}(g)\) is an ODE on a finite-dimensional space and Mathlib’s Picard–Lindelöf suffices. The development lives purely at the level of a finite-dimensional real normed space carrying a bracket, and shares no machinery with the rest of this blueprint — no CovariantDerivative, no vector bundles, no RiemannianBundle. Neither the analysis gap nor Theorem 7 is on its path.
Two representation choices earned this. The bracket is carried as an explicit map rather than through [LieRing]: that class and NormedAddCommGroup both extend AddCommGroup, an unresolved diamond with no precedent in Mathlib, so with a norm in play the bracket must leave the instance system. A transport bridge restates the results for genuine Lie algebras, so no generality is lost. And the metric is carried as a map into the dual, which makes smoothness a chain of contDiffAt_map_inverse and composition lemmas rather than coordinates and Cramer’s rule.
For left-invariant fields the Koszul formula
determines \(\nabla \) algebraically, so it can be defined rather than shown to exist.
\(\nabla _X Y - \nabla _Y X = [X,Y]\), and \(\langle \nabla _X Y, Z\rangle + \langle \nabla _X Z, Y\rangle = 0\).
Any torsion-free, metric-compatible bilinear connection equals the Koszul connection.
This is the fundamental theorem of Riemannian geometry in the left-invariant world — the statement Theorem 7 still leaves open at manifold level, discharged here because the algebra needs no existence theory.
\(g\mapsto -2\operatorname {Ric}(g)\) is \(C^n\) at every nondegenerate \(g\), for every \(n\).
\(\operatorname {Ric}\) is a polynomial in \(g\) and \(g^{-1}\). Building every operator inside the algebra of continuous linear maps makes smoothness a mechanical chain of composition lemmas, with contDiffAt_map_inverse at the single non-polynomial node. Nondegeneracy of an inner product comes from positive definiteness plus a dimension count.
Through every left-invariant metric there is a solution of \(\partial _t g= -2\operatorname {Ric}(g)\) near each time \(t_0\), and it is unique as a germ at \(t_0\).
Picard–Lindelöf, via ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt for existence and ODE_solution_unique_of_eventually for uniqueness; the 2025 refactor means IsPicardLindelöf never has to be constructed by hand.
Stated as a germ, deliberately. An earlier version of this blueprint claimed a unique maximal solution. Mathlib has no maximal-solution theory: gluing local solutions along a maximal interval is routine mathematics but absent infrastructure. The honest statement is what is proved.