OAI/GroupTheory/PolycyclicRecognition/Geometry/RiemannianExponentialInputs.lean

The published regularity inputs needed for Lipschitz replacement

These retain regularity that the earlier topological/metric inputs deliberately discarded. Dixmier, Bull. Soc. Math. France 85 (1957), Theorem 3, p.120, gives a global exponential diffeomorphism for a simply connected solvable group with real adjoint roots. Lee, Introduction to Riemannian Manifolds, second edition (2018), Lemma 3.10(b), Problem 6-12(c) and Corollary 6.21 give the complete left-invariant metric and minimizing paths. Lemmas 2.53–2.54, especially the length comparison (2.22), give local Lipschitz compatibility of smooth coordinates and their inverses with that Riemannian distance.

Only smooth (∞) regularity is retained; analyticity is not needed by the application. The second input is precisely this coordinate consequence of the published length comparison, for the chosen tangent-space coordinates. It assumes no contraction, interpolation, quasi-isometry or height conclusion.