Foundational corpus mapping FC08 Lee

Status: Sweep II complete. C01–C22 and Appendices CA–CD mapped.

Canonical catalogue: FC08 — John M. Lee, Introduction to Smooth Manifolds.

Pinned project baseline: Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0. Current upstream Mathlib was refreshed 2026-09-07 to 5315eef9e4ffb98e0f89f278b765c50a149f66ca (Lean 4.34.0-rc2). Declarations outside the project pin are revision-specific reference-port routes unless an importable package route is independently justified.

Every canonical unit receives exactly one Sweep-II route: mathlib, project-existing, package-import, reference-port, or unmatched. Project source is searched first, followed by pinned/current Mathlib, open/current work, indexed search services, Reservoir/packages, broad discoverable Lean repositories, and local reference mirrors. Strict bundle semantics apply throughout.

Provenance contract for FC08 C01

Chapter 1. Smooth Manifolds FC08

Provenance contract for FC08 C02

Chapter 2. Smooth Maps FC08

Provenance contract for FC08 C03

Chapter 3. Tangent Vectors FC08

Provenance contract for FC08 C04

Chapter 4. Submersions, Immersions, and Embeddings FC08

Provenance contract for FC08 C05

Chapter 5. Submanifolds FC08

Provenance contract for FC08 C06

Chapter 6. Sard’s Theorem FC08

Provenance contract for FC08 C07

Chapter 7. Lie Groups FC08

Provenance contract for FC08 C08

Chapter 8. Vector Fields FC08

Provenance contract for FC08 C09

Chapter 9. Integral Curves and Flows FC08

Provenance contract for FC08 C10

Chapter 10. Vector Bundles FC08

Provenance contract for FC08 C11

Chapter 11. Covectors and Covector Fields FC08

Provenance contract for FC08 C12

Chapter 12. Tensors FC08

Provenance contract for FC08 C13

Chapter 13. Riemannian Metrics FC08

Provenance contract for FC08 C14

Chapter 14. Differential Forms FC08

Provenance contract for FC08 C15

Chapter 15. Orientations FC08

Provenance contract for FC08 C16

Chapter 16. Integration on Manifolds FC08

Provenance contract for FC08 C17

Chapter 17. de Rham Cohomology FC08

Provenance contract for FC08 C18

Chapter 18. The de Rham Theorem FC08

Provenance contract for FC08 C19

Chapter 19. Distributions and Foliations FC08

Provenance contract for FC08 C20

Chapter 20. The Exponential Map FC08

Provenance contract for FC08 C21

Chapter 21. Quotient Manifolds FC08

Provenance contract for FC08 C22

Chapter 22. Symplectic Manifolds FC08

Provenance contract for FC08 CA

Appendix A. Review of Topology FC08

Provenance contract for FC08 CB

Appendix B. Review of Linear Algebra FC08

Provenance contract for FC08 CC

Appendix C. Review of Calculus FC08

Provenance contract for FC08 CD

Appendix D. Ordinary Differential Equations FC08