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.

Connected sum descends to oriented h-cobordism classes

Statement

Assume ${A C}_{ω}$ . For $n \geq 5$ , oriented connected sum of smooth homotopy $n$ -spheres descends to oriented h-cobordism classes and defines an associative and commutative operation with the class of $S^{n}$ as identity.

Facts & Assumptions

Given: Oriented smooth homotopy $n$ -spheres with $n \geq 5$ , h-cobordisms $W : Σ_{0} \to Σ_{1}$ and $W^{'} : Σ_{0}^{'} \to Σ_{1}^{'}$ , and the orientation-compatible boundary identification used to form connected sums.

[A1]

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

[L1]

Connected sum of oriented homotopy spheres is again an oriented homotopy sphere for $n \geq 3$ (Connected sum preserves oriented homotopy spheres), and collar gluing and corner smoothing of cobordisms are available (Collar gluing and seam smoothing give transitivity, Smooth collars of a manifold boundary).

[L2]

An h-cobordism is a compact smooth cobordism triad whose two face inclusions are homotopy equivalences (h-Cobordism), and the faces arising here are closed and connected.

[L3]

Assume ${A C}_{ω}$ . Let $X$ be a compact smooth manifold with boundary, let $0 \leq k \leq \dim X$ , and let attaching embeddings $φ_{0}, φ_{1}$ of $S^{k - 1} \times D^{\dim X - k}$ into $\partial X$ extend over a neighbourhood of the disk factor and be joined by a smooth isotopy through such embeddings that is constant near the ends of the parameter interval. Then the corner-rounded handle attachments $X \cup_{φ_{0}} (D^{k} \times D^{\dim X - k})$ and $X \cup_{φ_{1}} (D^{k} \times D^{\dim X - k})$ are diffeomorphic by a diffeomorphism that is the identity outside a collar of the swept attaching regions, and any later handles attached to the swept region are carried along, so the two total manifolds are diffeomorphic as well (Isotopic attaching embeddings give diffeomorphic handle attachments).

[L4]

Under ${A C}_{ω}$ , every connected smooth h-cobordism of dimension at least six with closed simply connected faces is a product relative to the incoming face (The smooth simply connected h-cobordism theorem).

Proof

technique · direct

1.1L1L3A1givenconstruct

An oriented connected sum uses small coordinate disks and the fixed orientation-reversing linear reflection of their boundary coordinates, as in [L1]. Changes of small coordinate disks are joined by isotopies: shrink each disk within its chart, move its centre along a finite chain of charts on a path in the connected manifold, and move its oriented frame through $G L_{n}^{+} (R)$ : Gram–Schmidt deforms the positive triangular factor to identity and plane rotations deform the orthogonal factor to identity. On a sufficiently small disk each chart change is isotopic to its derivative by rescaling, retaining positive determinant; the finitely many stages yield the required isotopy. Reparameterize it to be stationary near its ends. Applying [L3] to a $1$ -handle joining the outgoing faces of two disjoint product collars transfers this isotopy to an orientation-preserving diffeomorphism of their connected-sum boundary. Thus coordinate-disk choices do not affect the sum. This argument asserts no independence under an arbitrary nonextendable boundary twist.

2.1step 1.1L2L4A1

By [L2] the h-cobordisms $W, W^{'}$ are connected and their faces are simply connected homotopy spheres. Their dimension is $n + 1 \geq 6$ , so [L4] gives orientation-preserving diffeomorphisms $f : Σ_{0} \to Σ_{1}$ and $f^{'} : Σ_{0}^{'} \to Σ_{1}^{'}$ : a product diffeomorphism relative to the incoming face preserves its orientation, and hence the orientation throughout the connected cobordism. Choose outgoing disk charts by transporting the incoming ones through $f, f^{'}$ . The restrictions of $f, f^{'}$ then agree with the coordinate reflection used at the neck and glue to an orientation-preserving diffeomorphism $Σ_{0} # Σ_{0}^{'} \to Σ_{1} # Σ_{1}^{'}$ . Its product cylinder is an oriented h-cobordism. Step 1.1 removes dependence on the disk choices, proving descent to classes.

3.1step 1.1step 2.1construct

For three summands choose two disjoint small disks in the middle one and one disk in each outer one. Both groupings are the same quotient of the three punctured manifolds with the same two neck identifications; regrouping the quotient gives an orientation-preserving diffeomorphism. Interchanging the summands reverses the neck parameter and applies the fixed reflection on its sphere factor, so the two orientation signs cancel and give an orientation-preserving diffeomorphism. Together with step 1.1 these prove associativity and commutativity.

4.1step 1.1step 3.1L1

The complement of a standard coordinate disk in $S^{n}$ is a standard disk. The coordinate reflection extends linearly over it, so gluing this complement into the removed disk of $Σ$ restores $Σ$ orientation-preservingly. Thus $S^{n}$ is an identity; [L1] ensures that every sum remains a homotopy sphere.

5.1step 2.1step 3.1step 4.1∎

Connected sum consequently defines the asserted associative, commutative operation on oriented h-cobordism classes with identity $[S^{n}]$ .

Depends on

Used by

The homotopy-sphere group Θₙ Definition
Parallelizable boundaries form a subgroup Lemma

Dependency tree · two levels

89 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

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