Add optimal transport and Wasserstein geometry roadmap

[Vilin97]

Summary

• add a definitive 17-layer, dependency-ordered roadmap for optimal transport and Wasserstein geometry
• make Brenier's theorem and polar factorization, Monge--Ampère regularity, Benamou--Brenier, Wasserstein gradient flows/JKO, barycenters, entropic transport/Sinkhorn, synthetic curvature, and Gromov--Wasserstein required milestones
• add compiled representative signatures, in roadmap order, for raw couplings/costs, Wasserstein components, Monge/Kantorovich maps, the map-facing quadratic transport conclusion, Fréchet/Chebyshev centers, and finite Sinkhorn scaling
• import the signature module from TauCetiRoadmap.lean

Generality and references

Villani's Optimal Transport: Old and New is the classical spine, supplemented by Ambrosio--Gigli--Savaré and Lisini for dynamic transport and gradient flows, De Philippis--Figalli/Caffarelli/MTW for regularity, and primary sources for barycenters, Schrödinger/Sinkhorn, CD/RCD theory, Alexandrov-space maps, and measured-kernel GW. It is a source map rather than a chapter-by-chapter transcription.

Definitions begin at the weakest mathematically valid level—raw measures, extended costs, arbitrary measurable carriers, extended exponents, and target-valued measured kernels. Standard-Borel, Polish, Euclidean, Riemannian, curvature, finite-cost, compactness, and regularity assumptions remain local to the theorems that need them. Each milestone asks for the strongest valid form with its real hypotheses exposed, plus counterexample guardrails where common overgeneralizations fail.

Lean prior art and coordination

The roadmap audits and pins:

• Joseph Miller's Apache-2.0 Vlasov W₁ development at 31186ee11b1c478a35b1775db48384252eb06e22
• Daniel Lyng's Apache-2.0 Econlib OT development at 003655ccf010cdf44c4f67d6675167b54ce0e9df
• Quang Dao and Devon Tuma's Apache-2.0 VCVio discrete-coupling development at a5f474fd0e9a26266cc599d100267411690dfeb7
• the LeanTriathlon Sinkhorn and incomplete Brenier prototypes

It requires coordination before adapting those sources. A pinned-Mathlib audit used Lean LSP searches to reuse existing law, conditional-kernel/disintegration, trajectory/projective-limit, convexity/Rademacher, KL-divergence, probability-measure, and compact Gromov--Hausdorff APIs rather than proposing duplicates.

The root roadmap list and issue dropdowns are intentionally unchanged: TauCetiRoadmap/ is the source of truth, and the repository's post-merge sync workflow owns those generated copies.

Review preemption

• reconciled Suggested.lean with the README's dependency order
• ran independent source/correctness and Mathlib-reuse/dependency audits
• kept public Lean docstrings declaration-focused and renamed targets to match their conclusions
• ran TauCetiReview manually in non-posting mode against exact head 687b16593fb40c4768513d35aeb86d6295c10e32; all ten rubrics approved

Validation

• lake build (8,521 jobs; expected roadmap sorry warnings only)
• lake env lean TauCetiRoadmap/OptimalTransport/Suggested.lean
• Lean LSP diagnostics: nine expected sorry warnings, no errors
• codespell TauCetiRoadmap/OptimalTransport/README.md TauCetiRoadmap/OptimalTransport/Suggested.lean --ignore-words-list=OT,AGS,Savin
• git diff --check
• TauCetiReview exact-head manual dry run: all ten rubrics approved
• check_roadmap_areas.py reports only the expected generated-index drift; the sync workflow fixes it after merge

Authorship

Prepared with OpenAI Codex, including independent research and adversarial review agents; mathematical and API findings were checked against the cited primary sources and pinned Mathlib.

[Vilin97]

@kim-em , lmk if this looks good