ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck pass

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.

Handle slides change the matrix but not the Whitehead torsion

Example

Assume ${A C}_{ω}$ . In the right-module convention, let $A : C_{q + 1} \to C_{q}$ be the differential matrix of a two-index high-dimensional h-cobordism presentation, $2 \leq q \leq n - 2$ , $\dim W = n + 1 \geq 6$ . Slide the $j$ th lower handle over the $i$ th with signed label $r = \pm g$ , so its new core basis vector is $e_{j}^{'} = e_{j} + e_{i} r$ . Put $P = I + E_{i j} r$ . Then the new differential matrix is $P^{- 1} A$ , and the torsion class is unchanged. A single slide adds one signed group monomial; a general group-ring coefficient is realized by a finite sequence.

Facts & Assumptions

Given: The presentation and the nonzero signed monomial $r = \pm g$ , with $i \neq j$ , in the statement.

[F1]

The chosen handle generators form a right basis; lower handles index rows and upper handles index columns of the differential. The based handle chain complex over the fundamental group ring.

[F2]

Slides preserve presentation-indexed torsion, and elementary basis matrices have zero Whitehead class. Handle slides and cancelling-pair creations preserve Whitehead torsion, Cellular basis ambiguities vanish in the Whitehead group.

[F3]

In degrees $q, q + 1$ the torsion is $(- 1)^{q} [A]$ . Presentation-indexed Whitehead torsion of an h-cobordism.

Verification

1.1F1givenalgebra

In the old target coordinates the new basis has columns $e_{k}^{'}$ , hence matrix $P = I + E_{i j} r$ , with $P^{- 1} = I - E_{i j} r$ . The source basis is unchanged. Since an old target coordinate column equals $P$ times its new column, the new differential is $A^{'} = P^{- 1} A$ . Thus row $i$ changes by subtracting $r$ times row $j$ . The target core change acts inversely on differential coordinates; it must not be copied directly onto the belt basis.

2.1step 1.1algebra

For the concrete matrix $A = I_{2}$ , take $i = 1, j = 2, r = 1$ . Then $P = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ and $A^{'} = (\begin{array}{cc} 1 & - 1 \\ 0 & 1 \end{array}) \neq I_{2}$ . Both are invertible. More generally $P^{- 1} A = A$ for an invertible $A$ would imply $P = I$ , impossible for $r = \pm g$ .

3.1F2F3step 1.1step 2.1∎

By [F2], $[P] = 0$ and $[P^{- 1} A] = - [P] + [A] = [A]$ in the Whitehead group. Multiplying by the parity sign in [F3] gives $τ_{H^{'}} = τ_{H}$ . This supplies the promised matrix computation and the unchanged torsion class.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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)