Review Issues — OpenGA Hopf–Rinow Formalization

[JxChen24]

Review Issues — OpenGA Hopf–Rinow Formalization

(Review of MathNetwork/OpenGA, branch feat/hopf-rinow, against do Carmo,
"Riemannian Geometry", Ch. 7, Theorem 2.8 — site: Chapter 9, Theorem 9.12.)

Preamble. This review is AI-polished, not AI-generated. The issues below
were found and examined independently by me, and I take full responsibility
for their accuracy; AI assistance was used for wording, for cross-checking
claims against the sources, and for formatting. I'm not certain the fixes I
propose are the right ones — they're starting points — which is why this is
an issue rather than a pull request. The review is long and meant to be processed
by AI first. The exact fixes are less important than the questions on formalization
standards posted in the end of this issue.

1. A Major Issue

The exponential map currently formalized as Riemannian.Exponential.expMap is
strictly a local, chart-anchored object: it is defined via the maximal integral
curve of the geodesic field in the single fixed chart at the base point, and it
represents the true geodesic only while the geodesic stays in that chart.

1.1 Source of the problem

do Carmo defines exp in Ch. 3 (after Remark 2.8), noting that "in most of the
applications" only a restriction of exp to an open subset of T_qM is needed.
Geodesic completeness (Ch. 7, Def. 2.2) is not such an application: it
quantifies exp_p over all of T_pM. Def. 2.2 gives two phrasings joined by an
"i.e." — one via the exponential map, one via geodesics defined for all
parameter values. Only the latter is formalized (IsGeodesicallyComplete),
because the current expMap cannot express the former:
expDomain g p = Set.univ can fail even on a complete manifold (the round
circle — the counterexample given in HopfRinow.lean's own module docstring).
The misalignment therefore reaches Theorem 2.8 in both a) and d): a) is stated
in exp language while its Lean counterpart (the hypothesis hp of the _at
theorems) is in geodesic language, and d) rests on Def. 2.2, whose exp-phrased
half is unformalized. The equivalence of the two phrasings is nowhere
formalized. Statements b), c), e), f) are unaffected (purely metric, no exp).

1.2 Essence of the problem

This is neither a mathematical error nor an ordinary single-statement
mismatch. If the geodesic phrasing is adopted uniformly, the proved theorems
are correct and self-contained, and the substitution is licensed by do Carmo's
own "i.e." in Def. 2.2. Under a stricter math–Lean alignment standard,
however, the book states Hopf–Rinow in exp language, and that language is
connected to the Lean development only by prose.

1.3 Proposed fix

Minimal: keep the formalization but document the substitution visibly on the
Def. 2.2 and Thm. 2.8 nodes (which phrasing was formalized, and why the
current expMap must not be used to state them). Full fix (recommended):
define the intrinsic, chart-glued global exponential map; define exp-phrased
geodesic completeness; prove the equivalence of the two definitions (e.g.
expDomain g p = Set.univ ↔ ∀ v, hp v); and re-anchor a) and d) through it.
Note that the Hadamard theorem in the same chapter makes the global
exponential map unavoidable anyway — there exp_p is the subject of the
statement, not notation.

2. Comments on the website

2.1 Numbering

The site's chapter/theorem numbers (9.12) differ from do Carmo's own numbering
(Ch. 7, Thm 2.8), since the LaTeX counters simply number the included chapters
sequentially. That is fine in itself, but the book coordinates are already
recorded in the source (\dcref{ch7:2.8}, and labels like thm:dc-ch7-2-8) —
it would help readers working with the book side by side if the rendered node
displayed this provenance, e.g. "do Carmo Ch. 7, Theorem 2.8" under the title.

2.2 A natural-language/Lean mismatch in the displayed node

The natural-language part of the Theorem 9.12 node states the full Hopf–Rinow
theorem (a–e equivalent, f a consequence), but the Lean part lists only four
theorems, covering (a ⟹ c), (c ⟺ d), (c ⟹ f), and (a ⟹ b). The missing
directions are exactly the content of Lemma 9.13 (b ⟹ c) and Lemma 9.14
(b ⟺ e). These lemmas are cited in the proof of Theorem 9.12 — both in the
proof text ("This is Lemma 9.13/9.14") and in the proof-level \uses — but the
website appears to render neither the proof text nor the proof-level
dependency edges on the node, so the delegation is invisible, and the node
initially reads as an incomplete formalization. Suggested fix: render the
proof (even collapsed) and/or the proof-level \uses links on the node. (The
underlying statement-level gap is Section 3.2 below.) Note that in the branch
source the Theorem 2.8 node carries no \leanok — the source honestly does
not claim the node fully formalized; if the website renders it as complete,
that is a rendering or version divergence worth checking.

3. Comments on the Lean code

3.1 Misleading name hopfRinow

The Lean theorem hopfRinow is the (c ⟺ d) statement only —
CompleteSpace M ↔ IsGeodesicallyComplete g — not the full Hopf–Rinow
theorem. It should be named complete_iff_isGeodesicallyComplete (or
similar), with the headline name reserved for the full statement.

3.2 No Lean theorem states the full Hopf–Rinow theorem

Currently no single Lean theorem corresponds to do Carmo's Theorem 2.8 as a
whole; the claim that the existing fragments jointly constitute it lives only
in prose (blueprint proof, README, module docstring). I suggest adding one — a
conjunction of the equivalences plus the f) corollary, proved by invoking the
existing declarations — and anchoring it on the node. This closes the
statement-matching gap at the cost of a few dozen lines of glue.

3.3 The distance is defined over a different curve class than in the book

do Carmo (Ch. 7, Def. 2.4) defines the distance as the infimum of lengths of
piecewise differentiable curves; the formalization anchors this to Mathlib's
riemannianEDist, whose infimum runs over C¹ paths. The two infima coincide
mathematically (corners can be smoothed by reparametrizing each piece to zero
velocity at the junctions, preserving length), but this equivalence is neither
formalized nor mentioned, and the Def. 2.4 node is marked \leanok as if the
rendering were literal. The cheap fix is a remark on the node recording the
substitution. The expensive fix is to formalize the equivalence — ideally as a
Mathlib lemma, since it concerns riemannianEDist and not do Carmo; note that
a genuine piecewise-curve API will be needed anyway for the variational
chapters (broken geodesics, first/second variation).

3.4 Continuity is not part of the definition of a geodesic

The Lean predicate IsGeodesic requires only the geodesic equation
HasGeodesicEquationAt at every time; it does not require Continuous γ, and
continuity is not derivable from it: the equation reads γ through
extChartAt, which junk-extends outside its chart source, so a discontinuous
curve whose junk chart readings happen to vary smoothly can satisfy the
equation (the authors' docstrings acknowledge this). In do Carmo no such
clause is needed because his standing convention (Ch. 0: "differentiable"
means C^∞) makes every curve smooth — in particular continuous — before the
geodesic condition is imposed; the faithful counterpart of the book's
"geodesic" is therefore the conjunction Continuous γ ∧ IsGeodesic g γ.
All statements in the current dependency cone pair the two correctly, but the
invariant is enforced only by convention, not by the definitions. Suggested
fix: either introduce a bundled notion (e.g. IsGeodesicCurve :=
continuity + equation) for all public-facing statements, or rename the naked
predicate to something like SatisfiesGeodesicODE so it cannot be mistaken
for the book's geodesic, plus a remark on the relevant blueprint nodes.

3.5 Status question: the length-space bridge in the parent repository

The module docstring of HopfRinow/EVariationLePathELength.lean refers to a
"remaining sorry" in Bridges/RiemannianToLength.lean — a file of the full
OpenGA repository, not of this branch — for the hard half of the length-space
bridge (⨅ γ, pathLength γ ≤ edist x y, i.e. that the Riemannian distance is
intrinsic in the metric-geometry sense). The Hopf–Rinow milestone cone is
unaffected: the Bridges file is absent from the cone, the cone contains no
sorry, and the only results it consumes from this circle of ideas
(edist_le_pathELength_of_cmdiff, LengthSpace.edist_le_pathLength) are
fully proved. Notably, this branch supplies the missing analytic core
(eVariationOn_le_pathELength), and the docstring records the one-line term
that discharges the sorry once it is hooked in. Question to the
maintainers: has that sorry now been discharged, and if so, can the
docstring reference be updated?

3.6 Statement f) is rendered as a distance identity, not a length identity

do Carmo's f) asserts a geodesic joining p to q with ℓ(γ) = d(p, q).
The anchored theorem exists_minimizing_geodesic concludes instead
dist (γ s) (γ t) = |s − t| * dist x y for all s, t ∈ [0, 1] —
parametrization proportional to arc length, minimizing on every subsegment.
This implies (and is stronger than) the book's statement, but the literal
curve-length equation is never stated, even though the bridge material exists
in the cone (eVariationOn_le_pathELength). Cheap fix: a corollary stating
the length identity, or a node remark recording the substitution. Related:
the a) ⟹ f) form (exists_minimizing_geodesic_of_forall_geodesic), which
matches do Carmo's proof object verbatim (including his equation
d(γ(s), q) = d(p, q) − s), exists in the library but is not anchored on the
node.

4. Minor remarks

• Dimension 0 excluded. The standing hypothesis NeZero (Module.finrank ℝ E)
  silently restricts all results to dimension ≥ 1. Nothing false is claimed
  (the 0-dimensional connected case is a point, where Hopf–Rinow is trivial),
  but the exclusion is undocumented.
• Docstring letter labels. The engine docstrings in
  Exponential/ProperAssembly.lean label themselves "f) ⟹ b)" and "f) ⟹ c)"
  where, by the file's own a)–f) labeling, the hypothesis is a)-at-a-point.
  One-line doc fix.
• Graph shows the book's route, not the code's. The proof-level \uses of
  the Theorem 2.8 node cites thm:dc-ch3-3-7 (totally normal neighborhood),
  per do Carmo's argument, while the Lean proof consumes the uniform-flow
  substitute (exists_uniform_geodesic_flow) instead. Both proof-route
  substitutions (totally normal neighborhood → uniform Picard–Lindelöf flow in
  c ⟹ d; normal balls → chart-Lipschitz comparison in positivity of d) are
  disclosed in the blueprint prose and are unobjectionable; only the
  dependency edge is slightly misleading.
• Regularity of geodesics. HasGeodesicEquationAt demands only pointwise
  twice-differentiability of the chart reading, versus the book's C^∞ curves —
  a deliberate generalization, used consistently on both sides of every
  equivalence. That Lean-geodesics are in fact smooth (ODE bootstrap) is true
  but not formalized, and not needed for these theorems.

Questions for discussion

1. Several statements in this review are formalized under a paraphrase of the
   book's wording (Sections 1, 3.3, 3.6). What criterion should the project
   adopt for when a paraphrase is an acceptable rendering of a blueprint
   statement, and how should accepted paraphrases be documented?

2. How should the intrinsic (chart-glued) exponential map be defined in our
   framework — its domain, and the construction it rests on — and what should
   the precise statement of its equivalence with IsGeodesicallyComplete be?

3. What form should a single Lean statement of the full Theorem 2.8 take — in
   particular, how should a)'s "for one, equivalently every, p" be rendered,
   and how should the typeclass-valued statements (ProperSpace,
   CompleteSpace) be combined with the pointwise ones?

4. Which public names in the Hopf–Rinow dependency cone would require changes
   under Mathlib naming conventions, and what naming rule should the project
   fix going forward?

[Xinze-Li-Moqian]

Triage & plan (maintainers). Thanks @JxChen24 — exactly the kind of review the project wants.

Scope: the website / book-faithfulness items (§2, and §3.3's do-Carmo-vs-C¹ wording) are deprioritized — the project doesn't bind itself to do Carmo's exact statements.

The substantive code findings are accepted. Per our release discipline (main carries no sorry and no known-flawed code — we don't adopt-then-churn), they should be fixed on feat/hopf-rinow before the affected files are adopted into main. Now tracked as adoption prerequisites in milestone v0.1.0 — Hopf–Rinow:

• §3.4 — naked IsGeodesic / HasGeodesicEquationAt carries no continuity (and it isn't derivable). Bundle continuity (IsGeodesicCurve) or rename the ODE predicate (SatisfiesGeodesicODE). Blocks Geodesic/Equation.lean and its downstream (incl. FiberScaling, most of L1+).
• §3.1 — hopfRinow currently names only c ⟺ d; rename to complete_iff_isGeodesicallyComplete and add a full-theorem hopfRinow. Blocks the HopfRinow.lean finale.
• §1 / §3.6 — chart-local expMap and the distance-vs-length form: noted for later.

@AxelDlv00 — could you take §3.4 and §3.1 on feat/hopf-rinow? Those two gate the middle/finale layers of the adoption.

[Xinze-Li-Moqian]

@AxelDlv00 — concrete locations + fix sketches for the two prerequisites (permalinks pinned to feat/hopf-rinow @ 3d2a4bea6996).

§3.4 — IsGeodesic carries no continuity

Current defs in Geodesic/Equation.lean:

• IsGeodesic L556-557
• IsGeodesicOn L570-572
• HasGeodesicEquationAt L383-391

def IsGeodesic (g) (γ : ℝ → M) : Prop :=
  ∀ t : ℝ, HasGeodesicEquationAt g γ t          -- no Continuous γ

Because HasGeodesicEquationAt reads γ through chartLocalCurve (i.e. extChartAt, which junk-extends outside its source), a discontinuous γ whose chart readings happen to vary smoothly satisfies ∀ t, HasGeodesicEquationAt. Continuity is neither required nor derivable.

Fix (either):

-- A) honest rename — it only satisfies the ODE, doesn't claim to be a geodesic
def SatisfiesGeodesicODE (g) (γ : ℝ → M) : Prop := ∀ t, HasGeodesicEquationAt g γ t
-- B) bundle continuity for all public-facing statements
def IsGeodesicCurve (g) (γ : ℝ → M) : Prop := Continuous γ ∧ ∀ t, HasGeodesicEquationAt g γ t

§3.1 — hopfRinow names only c ⟺ d

hopfRinow L134-138:

theorem hopfRinow (g) [ConnectedSpace M] (hg : g.IsRiemannianDist) :
    CompleteSpace M ↔ IsGeodesicallyComplete g := …   -- only the equivalence

Fix: rename this to complete_iff_isGeodesicallyComplete, and reserve hopfRinow for a real full statement conjoining the existing fragments (complete_of_geodesicallyComplete_at, exists_minimizing_geodesic), with the minimizing curve stated via the continuity-bundled predicate from §3.4.