Skip to content

Coverage contract

This project formalizes selected results from Hatcher's Algebraic Topology; it does not claim to formalize the whole book. The canonical artifact is a project-authored, citation-only execution ledger rather than redistributed book text. Its thirty-two lines record seventeen decomposed source areas, thirteen explicitly deferred areas, and two areas outside scope. Every decomposed row links directly to its formalizable roadmap leaves.

Unit Area Lines Locator Unit SHA-256 Coverage Evidence
hatcher-1-1-basic-constructions §1.1 Basic constructions 1-1 Hatcher §1.1, pages 25–38 d4babbb34e3035c1ee16fbc7e6b707dbf0c17c3cfacf0ef8834756326f8b9a00 DECOMPOSED The selected section is decomposed into its explicit source-facing and Mathlib-backed leaves. Straight-line homotopy between paths, Borsuk–Ulam for the two-sphere, Brouwer's fixed point theorem for the disc, A path induces change of basepoint, The real line covers the circle, Convex sets have trivial fundamental group, Euclidean two-space is distinguished by dimension, The fundamental group of the circle, Path concatenation gives the fundamental-group law, The fundamental theorem of algebra, Homotopic maps differ by basepoint change, A homotopy equivalence induces a fundamental-group isomorphism, A loop splits across an open cover, The circle is not a retract of the disc, Path homotopy is an equivalence relation, The fundamental group of a product, Retractions and deformation retracts on the fundamental group, Simply connected spaces have unique path-homotopy classes, Higher spheres are simply connected, Three closed sets covering the sphere contain an antipodal pair, The fundamental group of the torus, Winding number of a loop in the circle
chapter-0-underlying-geometric-notions Chapter 0, underlying geometric notions 2-2 Hatcher Chapter 0, pages 1–20 0c3060a7dd102a89e57b59c842194aa76f56691f210b8e7becdb3ea196da6d21 DEFERRED Deferred to a future roadmap milestone; the current chapter page is an informational map.
hatcher-1-2-selected-spine §1.2 selected spine 3-3 Hatcher §1.2, pages 40–55 6743c757054319ea82b98fd0c8e7ae9d405b7f22117053bda8573a635dacc8a9 DECOMPOSED The selected van Kampen, wedge, cell-attachment, presentation-complex, and classical-CW bridge spine is decomposed into formalizable leaves. Classical skeleton inclusions are abstract cell attachments, Classical and standard cells have isomorphic attaching arrows, A successor classical skeleton has the cell-attachment quotient topology, The 2-skeleton of a path-connected CW complex is path-connected, Attaching higher cells preserves the fundamental group, Higher-cell attachments preserve path components, Finite skeleta above dimension two have the same fundamental group, Attaching 2-cells adds the attaching relations, The attaching-sphere pieces generate the intersection group, Binary van Kampen is a group pushout, An open-cover model for attached cells, Every abstract cell attachment has an indexed cone model, The strip enlargement retracts onto the attached space, The base-side auxiliary cover retracts onto the original space, Hatcher's binary cover of the strip enlargement, The strip-enlarged cell-attachment space, The auxiliary overlap has an indexed open cover, Each overlap piece has the homotopy type of its attaching sphere, The strip-connected upper cover is contractible, The auxiliary cover basepoint transports to the original basepoint, Overlap meridians recover the attaching loops, The boundary of the two-disk is the circle, An attachment with no cells is an isomorphism, An indexed cone attachment is a standard cell attachment, An indexed family of cone attachments is a topological pushout, A binary cover with a contractible second piece, A binary cover with a trivial second fundamental group, The degree-n circle map sends the generator to the degree-n loop, The circle is well-pointed at one, The cone on a disk boundary is the disk, The degree-n circle relation gives the cyclic group, An indexed family of cones has a two-set open cover, A single cone attachment is a standard cell attachment, The base-side cone cover retracts onto the original space, The single-cone cover intersection has the homotopy type of its boundary, A single cone attachment has a two-set open cover, A single cone attachment is a topological pushout, The cone-side cover member is contractible, Cover factorizations of a loop, The group presentation associated to an open cover, Overlap relations vanish under the cover map, The cyclic presentation complex, Every group is a fundamental group, Every group admits a generators-and-relations presentation, Elementary factorization moves preserve the quotient class, Homotopic factorizations have the same quotient class, A homotopy admits a threefold-incidence cover decomposition, The pointed wedge of a family of spaces, A point is one standard zero-cell, A wedge of circles is an indexed one-cell attachment, Collapsing the boundary of a one-disk gives the circle, Continuous maps out of a pointed wedge, Every fundamental-group element has a based disk-boundary representative, Eventually constant cell sequences form abstract CW complexes, Free-group relators form a standard two-cell attachment, Pointed wedges of path-connected spaces are path-connected, The identity attaches an empty family of cells, The presentation complex has the presented fundamental group, The presentation complex is an abstract two-dimensional CW complex, Presented groups have two-dimensional presentation complexes, The 2-skeleton determines the fundamental group, The kernel is generated by overlap relations, Van Kampen's quotient isomorphism, The van Kampen cover map is surjective, The fundamental group of a wedge of circles, The fundamental group of a wedge, The standard cover of a well-pointed wedge
hatcher-1-2-deferred-remainder §1.2 results outside the selected slice 4-4 Hatcher §1.2, pages 40–55 069343d0d5c388320af4a0fa3cd598b8db46f34ec6803b3c3c7fd1c46e3f90eb DEFERRED Examples 1.22–1.25, Corollary 1.27, and the geometric remainder of Example 1.29 are reserved for later application milestones.
hatcher-1-3-selected-spine §1.3 classification and deck spine 5-5 Hatcher §1.3, pages 56–82 881efdeb7a6e4db559c43675606e17063b7cfd6d3f1330c94de8e83c6536ed61 DECOMPOSED The selected lifting, universal-cover, classification, and deck-transformation spine is decomposed into formalizable leaves. Pointed connected covering spaces, The induced subgroup consists of loops with closed lifts, Changing the lifted basepoint conjugates the image subgroup, Covering maps inject path-homotopy classes, Covering-space actions give quotient coverings, The deck group is the normalizer quotient, A deck transformation is determined by one lifted point, Deck transformations and normal covers, The normalizer acts by deck transformations, The normalizer map is surjective with kernel the covering subgroup, Orbit quotients are normal and have the expected deck group, The orbit-quotient fundamental group recovers the acting group, Homotopies lift uniquely through a covering map, A map lifts exactly when its fundamental group lands in the covering subgroup, Local path-connectedness ascends along a covering, The fundamental group acts on a covering fiber, Pointed connected covers are classified by subgroups, Equal image subgroups characterize pointed cover isomorphism, Sheets are cosets of the induced subgroup, The subgroup cover realizes the chosen subgroup, The subgroup projection is a path-connected covering, The covering space associated to a subgroup, A lift is determined by one point, A simply-connected cover maps uniquely to every pointed connected cover, Small nullhomotopy neighborhoods form a basis, Semilocally simply-connected spaces, Universal-cover basis, The endpoint map is a covering, The path-class cover is path-connected, The path-class universal-cover space, The path-class cover is simply-connected, Connected covers are classified by conjugacy classes
hatcher-1-3-deferred-remainder §1.3 results outside the selected slice 6-6 Hatcher §1.3, pages 56–82 fa7d018b262c5f5800109b7c49e3f950f0bdccdd71952a41a1e06bf823f6efac DEFERRED Example 1.35, permutation classification, and Examples 1.41–1.48 are reserved for later milestones.
hatcher-2-1-selected-spine §2.1 singular-homology functoriality spine 7-7 Hatcher §2.1, pages 102–133 6d7497c44b12dc33b5df9d8dcf523a958b4f727b0d7908ea0e8e3badfdd347c6 DECOMPOSED The selected singular-chain, homology, and homotopy-invariance spine is decomposed into formalizable leaves. Chain-homotopic maps induce the same homology map, A chain map induces a map on homology, A homotopy equivalence induces homology isomorphisms, Homology of a point, The singular chain complex, Singular homology, Homotopic maps induce the same singular-homology map, A topological homotopy gives a singular-chain homotopy, Higher homology vanishes for totally disconnected spaces, Zeroth homology is free on path components
hatcher-2-1-relative-homology-les §2.1 reduced and relative homology with long exact sequences 8-8 Hatcher §2.1, pages 110, 113–118, and 127–128 aabcb68c9717f5f5cc063345b137ac95127096da3a30d2c72fcef63243928a65 DECOMPOSED The selected reduced- and relative-homology exact-sequence spine is decomposed into formalizable leaves. The augmented singular chain complex, Reduced singular homology, Reduced and ordinary homology agree in positive degrees, Zeroth homology splits at a basepoint, A short exact sequence gives an exact homology sequence, Relative homology of a simplicial-set pair, The singular set of a topological pair, Relative singular chains and homology, The long exact sequence of a pair, The pair long exact sequence is natural, A homotopy of pairs gives a relative chain homotopy, Homotopic maps of pairs induce the same relative-homology map, The reduced long exact sequence of a pair, The reduced pair long exact sequence is natural, Relative homology at a basepoint is reduced homology
hatcher-2-1-triple-les §2.1 long exact sequence of a triple 9-9 Hatcher §2.1, pages 118–119 and 127–128 cb575d45059f9973a268de41e1af526317b0554fa0930939db003c004314535e DECOMPOSED The selected triple exact-sequence slice is decomposed into four formalizable leaves. Topological triples and their maps, Relative chains of a triple form a short exact sequence, The long exact sequence of a triple, The triple long exact sequence is natural
hatcher-2-1-small-chains-excision §2.1 small chains and excision 10-10 Hatcher §2.1, pages 119–124 7131f31c731e5c0878b31b29a7e40792e5a02b758b5da1ebb31e0c65f38f604a DECOMPOSED The unit is decomposed into ten formalizable leaves. Affine barycentric subdivision, diameter contraction, affine-chain subdivision homotopy, singular-chain subdivision homotopy, eventual smallness, the small-chain equivalence, relative dévissage, chain-level binary excision, binary-cover homology excision, and deleted-subset homology excision.
hatcher-2-1-sphere-homology §2.1 reduced homology of spheres 11-11 Hatcher §2.1, pages 109–114 ad16b70f651b49dc7cd4c0610fb64ccd30b0bbd994a349d77e2de2e4408138da DECOMPOSED The reduced-homology foundations, S⁰ base case, and Corollary 2.14 are decomposed into six formalizable leaves. Homotopic maps induce the same reduced-homology map, a homotopy equivalence induces reduced-homology isomorphisms, reduced homology of a contractible space vanishes, the zero-sphere is a two-point space, reduced homology of the zero-sphere, and reduced homology of spheres.
hatcher-2-1-corollary-2-15 §2.1 Corollary 2.15 12-12 Hatcher §2.1, pages 114–115 2d49df5dc78a1e96159b707d0f66dca267c2b44abe7c114ea9d5225ec51f25c3 DECOMPOSED Corollary 2.15 is decomposed into three formalizable leaves. The boundary sphere is not a retract of the disk, a fixed-point-free disk map produces a boundary retraction, and Brouwer's fixed-point theorem for disks.
hatcher-2-1-good-pair-quotient §2.1 good pairs and quotient exact sequence 13-13 Hatcher §2.1, pages 114, 124, and 128 678963fee087b12085f82c43b5ebd6deb1664c995e5669a0269d22ccb68a2a02 DECOMPOSED The good-pair topology, Proposition 2.22, Theorem 2.13, and naturality are decomposed into fifteen formalizable leaves. Good pairs and neighborhood deformation retracts, functorial point quotients, point-quotient projection topology, the restricted quotient neighborhood, its contraction, the excision diagram, the componentwise relative criterion, the original-neighborhood comparison, the quotient-neighborhood comparison, the neighborhood excision comparison, pointed-comparison naturality, good-pair comparison naturality, Proposition 2.22, the quotient exact sequence, and its naturality anchor the complete DAG.
hatcher-2-1-post-excision-applications §2.1 post-excision applications 14-14 Hatcher §2.1, pages 125–126 1afb2ccc60da9538505a4cbd65feecc45306d38a78222a5675eb7362fa70b713 DECOMPOSED The mapping-cone comparison, Example 2.23, Corollaries 2.24–2.25, and Theorem 2.26 are decomposed into twenty-seven formalizable leaves. Mapping-cone model, contractible-subspace comparison, mapping-cone cover comparison, arbitrary-pair mapping-cone comparison, simplex boundary and horn, zero-horn retraction, simplex good pairs, zero-face point quotient, zero-face relative comparison, triple connecting formula, relative simplex fundamental class, simplex–disk pair homeomorphism, double-simplex cycle, double-simplex relative comparison, double-simplex fundamental class, double-simplex sphere homeomorphism, CW-subcomplex excision, sigma pointed pair, relative-chain coproduct, relative-homology coproduct, sigma good pair, wedge point quotient, wedge reduced homology, open-neighborhood local homology, contractible-ambient relative homology, punctured-Euclidean local homology, and invariance of dimension.
hatcher-2-1-deferred-remainder §2.1 remaining deferred results 15-15 Hatcher §2.1, pages 102–133 except the selected slices cc508cce1007b4939547650bd86946f185cbda2bfadd93e641359e1069177752 DEFERRED Proposition 2.6 beyond the selected S⁰ support, Δ-complex homology, Example 2.17, and Theorem 2.27 remain reserved for later milestones.
hatcher-2-2-mayer-vietoris §2.2 ordinary and reduced Mayer–Vietoris sequences 16-16 Hatcher §2.2, pages 149–150 15860684ed973c25411a01b97634ee5c0f0b5fe9d587d2009876cd5876011dea DECOMPOSED The core binary-cover construction is decomposed into six formalizable leaves. The binary-cover Mayer–Vietoris chain complex, binary-cover chains form a short exact sequence, the binary-cover Mayer–Vietoris sequence, small augmented chains include by a chain-homotopy equivalence, augmented binary-cover chains form a short exact sequence, and the reduced binary-cover Mayer–Vietoris sequence.
hatcher-2-2-mv-transport-sphere-recurrence §2.2 Mayer–Vietoris transport and sphere recurrence 17-17 Hatcher §2.2, page 150 bcebd7105f9477d8755b643e25bdcab20dd4577388bd196bd88214c51cae861a DECOMPOSED The neighborhood-deformation-retract extension and Example 2.46 are decomposed into nine formalizable leaves. Strong deformation retracts is the shared topology foundation. The ordinary neighborhood-retract Mayer–Vietoris sequence, the reduced neighborhood-retract Mayer–Vietoris sequence, a closed ball strongly deformation retracts from Euclidean space, a sphere strongly deformation retracts from punctured Euclidean space, stereographic models for hemispheres and the equator, the hemispheres have compatible neighborhood deformation retractions, the reduced homology of spheres satisfies the suspension recurrence, and reduced homology of spheres.
hatcher-2-2-degree-foundations §2.2 degree foundations 18-18 Hatcher §2.2, pages 134–135 4ddb04fda9f97f614f21124e055af2669c8ee2c2771e52b77b306a90dd2677fc DECOMPOSED Degree and properties (a)–(g), Theorem 2.28, and Proposition 2.29 are decomposed into sixteen formalizable leaves. Integral sphere orientation, degree definition, basic degree properties, punctured-sphere stereographic model, nonsurjective degree zero, double-simplex swap, coordinate sign changes, reflection degree, antipodal degree, fixed-point-free degree, tangent-field data, tangent-field parity obstruction, odd-sphere tangent field, Theorem 2.28, sphere-action degree character, and Proposition 2.29.
hatcher-2-2-local-degree §2.2 local degree and Proposition 2.30 19-19 Hatcher §2.2, pages 135–136 3b004b0c9c6a66f3cdb09112ac223353516aed14366675039bd9359d7f047f43 DECOMPOSED Local degree and Proposition 2.30 are decomposed into twenty formalizable leaves. Sigma topological pairs, relative-chain coproducts, relative-homology coproducts, disjoint open unions, deleted-pair neighborhood excision, disjoint punctured pairs, local sphere orientation, isolated-preimage neighborhoods, neighborhood local degree, shrinking invariance, well-defined local degree, the local-homeomorphism case, finite-fiber neighborhoods, finite-puncture pair excision, the homology coproduct, the projection matrix, the orientation sum, the local summand maps, the global degree square, and Proposition 2.30.
hatcher-2-2-computations-applications §2.2 results after Proposition 2.30 outside the selected Mayer–Vietoris slices 20-20 Hatcher §2.2, pages 136–159 after Proposition 2.30 except the selected material on pages 149–150 aa26b6e1351760242bed03ea98db284229f6420e3095c28132682ca18473f5e6 DEFERRED Examples 2.31–2.32, suspension invariance, cellular homology, Euler characteristic, homology of groups, the general CW-neighborhood construction, Examples 2.47–2.48, mapping-torus and relative Mayer–Vietoris sequences, and homology with coefficients remain reserved for later milestones.
hatcher-2-3-formal-viewpoint §2.3 Formal viewpoint 21-21 Hatcher §2.3, pages 160–165 d1104663ca164b82f33fd006b55060c996c602330693bfec4e61eba22530d4d7 DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
hatcher-3-1-cohomology-groups §3.1 Cohomology groups 22-22 Hatcher §3.1, pages 190–205 2b86cf2a2b961dd0eb7abaad041fb0b2323aa483988ebad9cf4934d250aca917 DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
hatcher-3-2-cup-product §3.2 Cup product 23-23 Hatcher §3.2, pages 206–229 9a816e99214134d16abfbabaa5b144b63f86513a80c9d0360be23121723f684f DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
hatcher-3-3-poincare-duality §3.3 Poincaré duality 24-24 Hatcher §3.3, pages 230–260 c9730782969b87332484c53febccb30ff3cc5dac191a40e4ff66a1ceb386d552 DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
hatcher-4-1-homotopy-groups §4.1 Homotopy groups 25-25 Hatcher §4.1, pages 339–359 fec386b117eff960f6af60f3ce0b6f7ba78bc098b450ae4cef69248167cc6fcb DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
hatcher-4-2-elementary-methods §4.2 Elementary methods 26-26 Hatcher §4.2, pages 360–392 e4e973e0c9d493c2f6ca59f1837bde6b4953e69df966a1d2f2d6fccd9f47aa53 DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
hatcher-4-3-connections-cohomology §4.3 Connections with cohomology 27-27 Hatcher §4.3, pages 393–420 3ff5e03e3ad165c3bad3234eb9670b1626ba3ab281f9f475f46cc494b052d134 DEFERRED Deferred to a future roadmap milestone; the current section page is an informational map.
appendix-proposition-a-1 Appendix Proposition A.1 28-28 Hatcher Appendix, Proposition A.1 974df7bb29f1375f810ff98cbde04e99fb81f1615e1a1637cf9cd987783030fa DECOMPOSED The compact-subspace theorem and its bounded-skeleton corollary are explicit leaves. Compact subsets lie in finite subcomplexes, Compact subsets lie in a bounded skeleton
appendix-proposition-a-5 Appendix Proposition A.5 29-29 Hatcher Appendix, Proposition A.5, pages 522–523 dd5b4ce0130e7ae454780da1a646fc9369032f359114caf4aef34e85252087bf DECOMPOSED The selected regular-neighborhood construction is decomposed into five formalizable leaves. Subcomplex intersection, cell-boundary collar, regular-neighborhood system, regular-neighborhood deformation retraction, and compatible subcomplex neighborhoods.
appendix-remainder Appendix remainder 30-30 Hatcher Appendix except Propositions A.1 and A.5 426efc3eaf0faa3c2f186837c8df48512187e7f9fc2abe123f9e4a8bbdc60632 DEFERRED Deferred to a future roadmap milestone; the current appendix page is an informational map.
lettered-additional-topics Lettered additional topics 31-31 Hatcher §§1.A–4.L 16905334d7dfc5520f9f89e337877212520b3800f320ecd22099601478df6a02 OUT Supplementary lettered sections are outside this project's main-line scope.
exercises Exercises 32-32 Exercise sets throughout Hatcher 6b62bc779713d6145d530fd369f5e6dfa8c241f508a7a4138ad3874d520a0fe7 OUT Exercise sets are not source targets for this project.

In scope

Hatcher §1.1, Basic constructions, pages 25–38, decomposed into twenty-two explicit nodes. The main target is Theorem 1.7, π₁(S¹) ≅ ℤ. The section's other in-scope results are:

Node Source result Kind
Straight-line homotopy between paths Example 1.1 cited
Path homotopy is an equivalence relation Proposition 1.2 pinned Mathlib
Path concatenation gives the fundamental-group law Proposition 1.3 cited
Convex sets have trivial fundamental group Example 1.4 pinned Mathlib bridge
A path induces change of basepoint Proposition 1.5 pinned Mathlib
Simply connected spaces have unique path-homotopy classes Proposition 1.6 pinned Mathlib
The real line covers the circle page 29, unnumbered bridged
Winding number page 29, unnumbered bridged
Fundamental group of the circle Theorem 1.7 cited
No retraction of the disc page 31, inside Thm 1.9's proof bridged
Brouwer for the disc Theorem 1.9 cited
Fundamental theorem of algebra Theorem 1.8 cited
The fundamental group of a product Proposition 1.12 cited
The fundamental group of the torus Example 1.13 cited
Loop splits across an open cover Lemma 1.15 cited
Higher spheres are simply connected Proposition 1.14 cited
Borsuk–Ulam for S² Theorem 1.10 cited
Three closed sets covering the sphere contain an antipodal pair Corollary 1.11 cited
Euclidean two-space is distinguished by dimension Corollary 1.16 cited
Retractions and deformation retracts on the fundamental group Proposition 1.17 cited
A homotopy equivalence induces a fundamental-group isomorphism Proposition 1.18 cited
Homotopic maps differ by basepoint change Lemma 1.19 cited

Three qualifications on what these nodes do and do not prove.

The opening results are explicit nodes. Propositions 1.2, 1.5, and 1.6 track the exact pinned declarations Path.Homotopic.equivalence, FundamentalGroup.fundamentalGroupMulEquivOfPath, and simply_connected_iff_unique_homotopic. Example 1.4 tracks the exact stronger input Convex.contractibleSpace; SimplyConnectedSpace.ofContractible and Mathlib's subsingleton fundamental-group instance give Hatcher's conclusion. Example 1.1 and Proposition 1.3 are local formalizations because they record Hatcher's explicit affine homotopy and left-then-right concatenation convention.

Theorem 1.8 is already upstream. Its statement is Mathlib's Complex.exists_root, packaged by Complex.isAlgClosed, in Analysis/Complex/Polynomial/Basic.lean and proved by Liouville's theorem. The local formalization gives a second proof of a known result. It is in scope as a source target and must not be counted as new Mathlib coverage.

Lemma 1.15 is reused by §1.2. It was formalized locally because Proposition 1.14 needed it, and it now supplies the surjectivity clause of Theorem 1.20 exactly as in Hatcher. The proof is adapted from the matching implementation in open Mathlib PR #28246. The overlap is recorded on the node.

§1.2 selected spine

Van Kampen's theorem is decomposed from its free-product presentation through the kernel calculation, wedge sums, cell attachments, and Corollary 1.28. Proposition 1.26 is split by part, and the Appendix compactness lemma needed for its 2-skeleton clause is a separate cross-chapter chain. The cover presentation, threefold-incidence homotopy decomposition, quotient form of van Kampen, pointed-wedge theorem, point-set cell-attachment model, strip cover, overlap analysis, and Proposition 1.26(a)–(b) are formalized. The classical successor-skeleton bridge, its 2-skeleton connectivity and finite-stage induction, and the independent presentation-complex route are formalized as well. All 67 leaves linked from the selected §1.2 unit are complete.

§1.3 selected classification and deck spine

Covering spaces is decomposed from homotopy lifting through the subgroup classification of connected covers. Exact pinned lifting results are separated from local source-facing wrappers. The path-class universal-cover construction, the fixed-universe quotient of pointed connected covers, and its cross-universe rigidity theorem are formalized. The deck-transformation branch continues through the normalizer quotient and orbit-action calculation in Propositions 1.39–1.40. All 32 leaves linked from the selected §1.3 unit are complete.

§2.1 selected slices

Simplicial and singular homology is decomposed through the singular-chain and singular-homology definitions, the exact H₀ calculation, the point calculation, induced maps, chain-homotopy invariance, topological homotopy invariance, and Corollary 2.11. Eight nodes are exact declarations in the pinned Mathlib; the point calculation and homotopy-equivalence corollary are formalized locally, so all ten linked leaves are complete. The project does not claim Hatcher's explicit prism formula is formalized.

Relative homology and exact sequences adds a fifteen-leaf second slice: the augmented definition of reduced homology, relative chains and homology, Theorem 2.16 and the long exact sequence of a pair, pair- and reduced-pair-sequence naturality, Example 2.18, and Proposition 2.19. All fifteen leaves are complete: the four-node reduced-homology branch, singular-pair functor, relative-homology functor, pair long exact sequence with its connecting-map formula and naturality, relative homotopy branch through Proposition 2.19, reduced pair sequence with its naturality, and pointed comparison are formalized locally, while the generic algebraic exact-sequence theorem and simplicial-pair foundation are present in the pinned Mathlib.

The same milestone now has a four-leaf triple-sequence slice: a project-authored topological-triple interface, the short exact sequence of relative chain complexes, its long exact homology sequence including the degree-zero endpoint, and naturality. All four leaves are formalized locally using the pinned pair and generic homology-sequence APIs; open Mathlib PR #41318 is prior art rather than an upstream dependency.

All ten leaves in the small-chains/excision slice are complete. Its subdivision, small-chain equivalence, relative dévissage, binary-cover chain-level comparison, and both homology-level excision endpoints are formalized locally.

§2.1–§2.2 selected Mayer–Vietoris, sphere, Brouwer, and degree slices

Mayer–Vietoris sequences are decomposed into six formalizable leaves. The selected slice constructs the binary-cover chain complex, proves its short exact sequence, transports its homology to ordinary singular homology, and packages the ordinary and reduced long exact sequences through their degree-zero endpoints. All six leaves are formalized locally and complete.

The sphere-homology milestone adds thirteen formalizable leaves. They cover reduced homotopy invariance and contractible vanishing, ordinary and reduced neighborhood-retract transport, the sphere-specific radial and stereographic geometry, Example 2.46's recurrence, the S⁰ base case, and the full reduced sphere calculation of Corollary 2.14. All thirteen leaves are formalized locally and complete.

Corollary 2.15 adds three leaves: the homological disk-boundary no-retraction theorem, the fixed-point-free boundary-ray retraction, and Brouwer's fixed-point theorem for positive-dimensional disks. All three are formalized locally and complete. The general §2.2 CW-subcomplex neighborhood extension beyond the selected Appendix A.5 support, and Examples 2.47–2.48, remain deferred with the rest of §2.2.

The good-pair quotient milestone decomposes Proposition 2.22, Theorem 2.13, and naturality into fifteen formalization leaves, all formalized locally and complete. Its shared strong-deformation-retract background leaf is also complete.

The post-excision applications milestone decomposes the arbitrary-pair mapping-cone comparison, Example 2.23, Corollaries 2.24–2.25, and Theorem 2.26 into twenty-seven formalization leaves. Its Appendix A.5 branch adds five regular-neighborhood leaves. All thirty-two leaves are formalized locally and complete.

The degree-foundations milestone decomposes Hatcher's degree properties (a)–(g), Theorem 2.28, and Proposition 2.29 into sixteen formalizable leaves. All sixteen are formalized locally and complete.

The local-degree milestone continues through Proposition 2.30 in twenty formalizable leaves. It plans the oriented local-homology class, neighborhood-independent local degree, the finite-puncture coproduct and projection calculation, and the sum of local degrees. These leaves are planned rather than asserted complete.

Deferred roadmap expansion

The remaining high-level section maps and retained source-unit remainders are explicitly deferred to future roadmap runs. Wholly deferred pages carry exposition and prior-art notes rather than formalization nodes:

Decomposing any of these is a future roadmap run, not proof work. Within Chapter 1, Example 1.35, permutation reconstruction, and Examples 1.41–1.48 remain deferred. Within §2.1, Theorem 2.20 and Proposition 2.21 are already decomposed into ten formalizable leaves, and Corollary 2.14 is now part of the sphere milestone. Corollary 2.15 is decomposed into three complete formalizable leaves. Theorem 2.13 and Proposition 2.22 are decomposed and complete in the good-pair milestone. Lemma 2.1 and Examples 2.2–2.5, Proposition 2.6 beyond the selected S⁰ support, Example 2.17, and Theorem 2.27 remain deferred. The mapping-cone comparison, Example 2.23, Corollaries 2.24–2.25, and invariance of dimension are decomposed in the post-excision milestone. Within §2.2, Examples 2.31–2.32 and their degree-realization calculations, suspension invariance, cellular homology, Euler characteristic, homology of groups, the general CW-neighborhood construction, Examples 2.47–2.48, mapping-torus and relative Mayer–Vietoris sequences, and homology with coefficients remain deferred.

Out of scope

  • Lettered Additional Topics. Sections 1.A, 1.B, 2.A–2.C, 3.A–3.H, and 4.A–4.L are excluded and have no roadmap pages. They are supplementary in the book and would double the mapping effort for material the main line does not depend on.
  • Exercises. Hatcher's exercise sets are not source targets.
  • Reproducing the text. The book is copyrighted and this repository is public, so /sources/ is gitignored. Source notes carry coordinates and one-line paraphrases only.

Done means

A local theorem-like node is complete when its named Lean declarations compile and its main result carries both statement: formalized and proof: formalized. A data-valued declaration has no separate proof phase and is complete when its main result compiles with statement: formalized. In both cases, the implementation uses no sorry and no axioms beyond Lean's three. A Mathlib-backed node is complete when its exact pinned declaration, kind, and declaring file pass provenance checks. CI performs these checks.

A section counts as finished only when it is decomposed and every node beneath it is complete, and nothing numbered in it has been deferred. By that rule §1.1 is finished. A section that is merely mapped is never finished, whatever its prose says.

The project as a whole makes no completion claim. Decomposing additional sections does not by itself imply that their nodes are formalized.