TheoremStatement: AI-adaptedProof: Literature-sourcedPipeline-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 Whitehead torsion of an h-cobordism is well defined for a fixed presentation and its elementary moves

Statement

Assume ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $(W; M_{0}, M_{1})$ be a nonempty connected smooth h-cobordism with a fixed finite handle presentation $H$ relative to $M_{0}$ . The class $τ_{H} (W, M_{0})$ is independent of the auxiliary choices in its definition: cellular representatives, basepoint paths, the universal-cover identification and chosen lifts, core orientations, the order of handles, and the chain contraction. If $H, H^{'}$ are related by the elementary handle modifications listed in Handle slides and cancelling-pair creations preserve Whitehead torsion, then $τ_{H} (W, M_{0}) = τ_{H^{'}} (W, M_{0})$ . For each fixed presentation it also agrees with AT-22's torsion of the inclusion $M_{0} ↪ W$ computed using the associated finite CW structure. No invariance under arbitrary changes of handle presentation is asserted.

Facts & Assumptions

Given: A nonempty connected smooth h-cobordism $(W; M_{0}, M_{1})$ and a fixed finite handle presentation $H$ of $(W, M_{0})$ .

[F1]

The presentation-indexed torsion is the contraction torsion of the based handle complex, taken in $Wh (π_{1} (M_{0}))$ , and by the comparison lemma it agrees with the Whitehead torsion of the inclusion $M_{0} ↪ W$ for the CW structure associated with the presentation (Presentation-indexed Whitehead torsion of an h-cobordism, The torsion of the handle complex is the torsion of the inclusion, The handle complex of an h-cobordism is contractible over the group ring, with an explicit contraction, The based handle chain complex over the fundamental group ring).

[F2]

AT-22's independence theorem: the Whitehead torsion of a finite CW homotopy equivalence is independent of the cellular representative, the basepoint paths, the universal-cover identification, the chosen lifts, the cell orientations and order, and the chain contraction; the contraction torsion of a contractible based complex is independent of the contraction (Whitehead torsion is independent of all auxiliary choices, Whitehead torsion of a finite CW homotopy equivalence, Contraction torsion does not depend on the contraction, Finite based free complexes and contraction torsion).

[F3]

Basis changes of the displayed handle bases given by elementary matrices, permutations, signs or units $\pm g$ die in the Whitehead group (Cellular basis ambiguities vanish in the Whitehead group).

[F4]

The elementary handle modifications of the listed kinds preserve the presentation-indexed torsion class (Handle slides and cancelling-pair creations preserve Whitehead torsion, Composition and based-pair sum formulas for Whitehead torsion, h-Cobordism).

Proof

1.1F1F3

The class $τ_{H} (W, M_{0})$ is defined as the contraction torsion of the based handle complex of the presentation, and by [F1] it equals the AT-22 torsion of the inclusion $M_{0} ↪ W$ for the associated finite CW structure; consequently the auxiliary choices made in the handle-complex definition (lifts of handles, core orientations, handle order) are exactly the choices controlled by the AT-22 independence theorem and the basis-change lemma.

2.1F2step 1.1

Independence of the chain contraction is the contraction-independence lemma for contraction torsion, and independence of the cellular representative, basepoint paths, cover identification, lifts, orientations and order is [F2] applied to the inclusion with the associated CW structures.

3.1F3F4step 2.1

If $H$ and $H^{'}$ differ by the listed elementary modifications, then by [F4] each modification preserves the class, so $τ_{H} (W, M_{0}) = τ_{H^{'}} (W, M_{0})$ ; this argument covers exactly the listed moves, and the elementary modifications of the previous lemma include cancelling-pair creation and deletion, handle slides of equal-index handles, reordering and re-choices of oriented lifts.

4.1F1step 3.1∎

Steps 2.1 and 3.1 give fixed-presentation auxiliary-choice independence and invariance under the listed elementary moves, and step 1.1 gives agreement with AT-22's torsion of the inclusion for the associated CW structure; nothing in the argument compares presentations that are not connected by the listed moves, so no invariance under arbitrary changes of handle presentation is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Presentation-indexed Whitehead torsion of an h-cobordism.

Dependency tree · two levels

72 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

Wolfgang Lück, A Basic Introduction to Surgery Theory (ICTP lecture notes, 27 October 2004; complete author text) (standard reference, not scraped)
Andrew Ranicki, Algebraic and Geometric Surgery (Oxford Mathematical Monographs, electronic edition) (standard reference, not scraped)