LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The two-disk complement of a homotopy sphere is an h-cobordism

Statement

Assume ${A C}_{ω}$ . For $d \geq 6$ , removing the interiors of two disjoint smoothly embedded closed $d$ -disks from a smooth homotopy $d$ -sphere $Σ$ gives a compact simply connected h-cobordism between two standard $S^{d - 1}$ boundary faces.

Facts & Assumptions

Given: A smooth homotopy $d$ -sphere $Σ$ with $d \geq 6$ and two disjoint smoothly embedded closed disks $D_{1}, D_{2} \subseteq Σ$ , with $W = Σ ∖ (int D_{1} \cup int D_{2})$ .

[A1]

Countable choice ${A C}_{ω}$ is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[L1]

Van Kampen computes the fundamental group of a union with connected overlap (Seifert–van Kampen identifies the fundamental group with a group pushout), and the colimit decomposition of $W$ with a disk reattached gives $W$ simply connected because the disks and the overlap collar are simply connected for $d \geq 6$ . [A1, given]

[L2]

Excision and the long exact sequence of the pair identify the homology of the complement of a disk with the homology of the punctured sphere, and the two-disk complement has the homology of $S^{d - 1} \times [0, 1]$ , with each boundary inclusion inducing an isomorphism in integral homology (Excision for singular homology, Long exact sequence of a pair, Mayer–Vietoris sequence in singular homology, Smooth homotopy sphere).

[L3]

Under ${A C}_{ω}$ every compact smooth manifold has a finite CW model, and the simply connected finite-model homology criterion derived in [L2] of Connected sum preserves oriented homotopy spheres applies (Compact smooth manifolds have finite CW models under countable choice, Relative Hurewicz comparison through a choice-free weak model, Whitehead theorem).

[L4]

An h-cobordism between closed smooth manifolds is a compact cobordism whose two face inclusions are homotopy equivalences (h-Cobordism).

Proof

technique · direct

1.1L1A1given

Removing finitely many disks leaves a path-connected manifold, since paths crossing them can be diverted along their connected boundary collars. Reattach the two disks successively to $W$ , using collar-thickened open covers; each overlap retracts to the simply connected $S^{d - 1}$ . Van Kampen [L1] shows that each reattachment preserves the fundamental group. The final space is $Σ$ , so $π_{1} (W) = π_{1} (Σ) = 0$ .

2.1step 1.1L2algebra

Orient $Σ$ . Excision identifies $H_{k} (Σ, W)$ with $H_{k} (D_{1}, \partial D_{1}) \oplus H_{k} (D_{2}, \partial D_{2})$ , zero except for $Z^{2}$ in degree $d$ . The map $H_{d} (Σ) = Z \to Z^{2}$ is $1 \mapsto (1, 1)$ , using the two local disk orientations. The pair sequence therefore gives $H_{d} (W) = 0$ , $H_{d - 1} (W) = Z^{2} / ⟨ (1, 1) ⟩ ≅ Z$ , and zero reduced homology in every other degree. Each boundary sphere maps to the class of its coordinate vector, up to its boundary-orientation sign, hence generates $H_{d - 1} (W)$ . Both face inclusions are integral homology equivalences.

3.1step 1.1step 2.1L3

By [L3] $W$ has a finite CW model. Transport each inclusion from the finite sphere to that model; step 1.1 gives simple connectivity, and step 2.1 gives homology equivalence. The finite-model homology criterion in [L3] makes each inclusion a homotopy equivalence.

4.1step 3.1L4∎

Thus the compact smooth $d$ -manifold $W$ , with its two standard sphere faces, meets exactly the definition of an h-cobordism [L4]. This proves the assertion for $d \geq 6$ .

Depends on

Used by

The Milnor homotopy seven-spheres are homeomorphic to S⁷ Corollary

Dependency tree · two levels

56 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Milnor, Lectures on the h-Cobordism Theorem, section 9, printed pp. 109-110 (standard reference, not scraped)
Michel Kervaire and John Milnor, Groups of Homotopy Spheres I, Annals of Mathematics 77 (1963), 504-537 (standard reference, not scraped)