Precondition for tagging v0.1.0: adopt the complete, sorry-free Hopf–Rinow proof from feat/hopf-rinow into main, one small reviewed PR at a time. Done when every PR is merged, main builds sorry-free (0 sorry / 0 axiom), and the do Carmo Ch.7 hopfRinow theorem lives on main. Then tag v0.1.0.

Release discipline

main is a release-quality branch and never contains sorry. Work-in-progress with sorry lives on a development branch and merges to main only once the proof is complete — enforced by a CI hard gate (sorry count must be 0; PR #113). The Hopf–Rinow theorem therefore returns to main only when its proof lands (the finale below), never as a sorry'd stub.

Workflow / roles

• Cut into small PRs — @LehengChen: slice feat/hopf-rinow into minimal, dependency-ordered PRs against main.
• Review — Axel Delaval & @JxChen24: assigned to each PR to check it.
• Approve & merge — Chunlei (@Spring-1211): final approval, then merge one at a time. (@Xinze-Li-Moqian delegates — Chunlei's approval suffices.)

Every PR must build green (Lake build + Sorry / axiom count) and be linked to this milestone.

Adoption plan — 41 new files, bottom-up in 16 layers

Merge in this order; each file is one small PR. (✅ merged · 🔄 in review)

• L0 — ✅ Topology/FiberBundleT2 (#110) · Geodesic/LinearODE · MetricGeometry/ProperExhaustion · Geodesic/FiberScaling · Geodesic/FlowDependence · Metric/RiemannianDistance
• L1 — Geodesic/CovariantDerivative · Geodesic/Homogeneity · Geodesic/VariationalEquation
• L2 — Geodesic/HopfRinow/MetricBridge · Geodesic/InitialVelocity
• L3 — Connection/ChartChristoffelChange · Exponential/Ray · Geodesic/ChartFlow · Geodesic/HopfRinow/ConstantSpeed
• L4 — Geodesic/DataTransfer · Geodesic/EquationTransfer · Geodesic/UniformExistence
• L5 — Exponential/StrictDerivative · Geodesic/FlowC1Dependence · Geodesic/FlowC2Dependence · Geodesic/FlowGeodesic · Geodesic/IntrinsicUniqueness
• L6 — Exponential/C2Ball · Exponential/StrictDerivativeBall · Geodesic/FlowReadback
• L7 — Exponential/LocalDiffeo · Exponential/RayODE
• L8 — Exponential/GaussLemma · Exponential/RayGeodesic
• L9 — Exponential/Minimizing · Geodesic/HopfRinow/GramBound
• L10 — Geodesic/Completeness · Geodesic/HopfRinow/CurveReadback
• L11 — Exponential/NormalBallEDist · Exponential/SegmentUpperBound
• L12 — Exponential/CornerRigidity
• L13 — Exponential/GrowthInduction
• L14 — Exponential/ProperAssembly · Geodesic/EndpointContinuity
• L15 — Geodesic/EndpointContinuityGlobal

Review #112 prerequisites (fix on feat/hopf-rinow first)

Substantive code findings from @JxChen24 (#112) must be fixed on the branch before the affected files are adopted (release discipline: don't adopt known-flawed code then churn). Owner: @AxelDlv00.

• §3.4 — the naked IsGeodesic / HasGeodesicEquationAt predicate carries no continuity and it is not derivable (junk chart extension). Bundle continuity (IsGeodesicCurve) or rename the ODE predicate (SatisfiesGeodesicODE). Blocks Geodesic/Equation.lean and its downstream (incl. FiberScaling, most of L1+).
• §3.1 — hopfRinow names only the c ⟺ d equivalence; rename to complete_iff_isGeodesicallyComplete and add a full-theorem hopfRinow. Blocks the HopfRinow.lean finale.
• §1 / §3.6 (later) — chart-local expMap; distance-vs-length form of the minimizing theorem.
  Website / book-faithfulness items (§2, §3.3) are deprioritized (project is not bound to do Carmo's exact wording).

Finale — 27 shared-file upgrades + the theorem

After the new files land, reconcile the 27 shared files that differ (case-by-case: some are already newer on main from cleanup, e.g. the linters; others need feat/hopf-rinow's proof-carrying versions — RiemannianMetric, Geodesic/Equation, Existence, MaximalInterval, HopfRinow.lean, …). The hopfRinow theorem itself lands with HopfRinow.lean. When main is sorry-free → tag v0.1.0.