Milestones
List view
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`.
No due date•1/6 issues closed