fix(MorganTian): port Issue 18 correspondence repairs

[AxelDlv00]

Summary

• Ports the completed Issue 18 correspondence repairs from OpenGA-Horizon onto main.
• Aligns the Chapter 1 blueprint with the Lean API: the continuity-aware geodesic predicate, regularity scopes, endpoint-explicit conjugacy, second variation/index-form mappings, injectivity/cut-time/radius scopes, Bishop–Gromov statements, and honest residual markers.
• The final diff contains only the two Issue 18 source files; no hgraph comments or review attachments are included.

Scope

This branch is based directly on main and intentionally excludes pending PR20 (graph/morgan-tian-issue-18-human-reviews). No PR20 commits, human-review importer, review-verdict files, or REVIEW_IMPORT artifacts are included.

Addresses #18.

Validation

• lake env lean MorganTianLib/Ch01/Geodesics.lean — passed.
• LAKE_NUM_THREADS=4 lake build in formalized-sources/MorganTian — passed (3669 jobs).
• Push-hook validation — MorganTian (3669), LeeRiemannian (3685), and Topping (8860) all passed with sorry=0 and zero standalone axioms.
• python3 blueprint/tools/check_tex.py blueprint/src/chapters/Ch01_Preliminaries.tex — passed.
• git diff --check — passed.