Raise the Hopf-Rinow development to Mathlib quality gates

[Spring-1211]

Summary

• add reproducible Lake build, test, declaration-lint, and text-style quality gates, together with GitHub Actions CI
• guard the exact axiom sets of the five main Hopf--Rinow facade theorems
• remove redundant finite-dimensional and completeness assumptions, and replace global unused-section-variable suppressions with precise declaration scopes
• measure heartbeat overrides, deleting eight of ten and localizing the two declarations that still need a higher limit
• introduce IsGeodesicallyCompleteAt as the reusable one-point predicate and document the facade's actual connectedness requirements

Motivation and impact

The branch was already sorry-free, but several engineering properties were not continuously checked and broad section assumptions obscured theorem generality. This PR makes those properties reproducible and brings the development closer to Mathlib's declaration, style, API, and CI expectations without changing the mathematical Hopf--Rinow conclusions.

The abstract ODE layer intentionally retains CompleteSpace E in its three Banach-space modules. The finite-dimensional Riemannian layer now relies on the instance supplied by FiniteDimensional ℝ E. Support for the zero-dimensional case is deliberately left for a separate mathematical generalization.

Validation

• lake build — 3005 jobs completed successfully
• lake test — exact axiom guards passed
• lake lint — declaration linting passed for OpenGALib
• lake exe lint-style OpenGALib — no diagnostics
• git diff --check upstream/feat/hopf-rinow...HEAD — no diagnostics

Static review also finds no sorry, admit, or unsafe token in the Lean sources and no remaining unusedSectionVars or unusedVariables linter suppression.

[vercel]

@Spring-1211 is attempting to deploy a commit to the xinze-li-bryan's projects Team on Vercel.

A member of the Team first needs to authorize it.

[AxelDlv00]

Nice cleanup — CI is green, no math changes, and the engineering wins are clear: axiom guards on the five facade theorems, tighter section hypotheses instead of a blanket unusedSectionVars suppression, most maxHeartbeats overrides gone, and IsGeodesicallyCompleteAt as a clean reusable one-point predicate. The failing Vercel check is unrelated to this PR (no Vercel step in the added workflow) and shouldn't block anything. LGTM.