ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

Torsion of a two-term based contractible complex

Statement

Let $R$ be a unital ring, let $u \in R^{\times}$ , and let $C_{∙}$ be the based right $R$ -chain complex $0 \to C_{q} = R \overset{u}{\to} C_{q - 1} = R \to 0$ for some $q \geq 1$ , with the displayed ordered right bases consisting of one vector in each of the degrees $q$ and $q - 1$ . Then:

$C_{∙}$ is contractible;
with the odd-to-even convention, $τ (C_{∙}) = (- 1)^{q + 1} [u] \in {\tilde{K}}_{1} (R),$ that is, $τ (C_{∙}) = [u]$ for odd $q$ and $τ (C_{∙}) = - [u]$ for even $q$ ;
after passing to $W h (π)$ the same formula holds for $R = Z [π]$ .

Facts & Assumptions

Given: A unital ring $R$ , a unit $u \in R^{\times}$ and the two-term based right $R$ -complex $C_{∙}$ concentrated in degrees $q - 1$ and $q$ with $q \geq 1$ and one basis vector per degree.

[F1]

A chain contraction of $C_{∙}$ is a right-linear family $s$ with $d s + s d = i d$ , the displayed right $R$ -bases make $C_{∙}$ a finite based free right $R$ -complex, and when the numbers of odd and even basis vectors agree the contraction torsion is the class $τ_{s} (C) = [A_{s}] \in {\tilde{K}}_{1} (R)$ of the matrix of $(d + s)_{o d d}$ in the degree-ordered displayed bases (Finite based free complexes and contraction torsion).

[F2]

The torsion class does not depend on the choice of contraction, so it is written $τ (C)$ , and the parity map $(d + s)_{o d d} : C_{o d d} \to C_{e v e n}$ is an isomorphism of right $R$ -modules for every contraction (Contraction torsion does not depend on the contraction, A chain contraction makes the odd-to-even parity map invertible).

[F3]

$K_{1} (R) = G L (R) / E (R)$ is written additively, so $[A B] = [A] + [B]$ , $[I] = 0$ and $[A^{- 1}] = - [A]$ ; ${\tilde{K}}_{1} (R) = K_{1} (R) / ⟨ [- 1] ⟩$ ; and $W h (π) = K_{1} (Z [π]) / ⟨ [\pm g] : g \in π ⟩$ receives the quotient map from $K_{1} (Z [π])$ (K₁ of a ring and the Whitehead group of a discrete group).

Proof

technique · direct

1.1

Write $e_{q}, e_{q - 1}$ for the displayed right-module basis vectors, so the matrix convention means $d (e_{q}) = e_{q - 1} \cdot u$ . Define the right-linear map $s$ by $s (e_{q - 1}) = e_{q} \cdot u^{- 1}$ and set its other components to zero. Then $d s (e_{q - 1}) = d (e_{q}) \cdot u^{- 1} = e_{q - 1} \cdot u u^{- 1} = e_{q - 1}$ , while $s d (e_{q}) = s (e_{q - 1} \cdot u) = e_{q} \cdot u^{- 1} u = e_{q}$ . Thus $d s + s d = 1$ in both nonzero degrees, so $C_{∙}$ is contractible with one odd and one even displayed basis vector.

1.2

If $q$ is odd then $C_{o d d} = C_{q}$ , $C_{e v e n} = C_{q - 1}$ and $s$ vanishes on $C_{q}$ , so $(d + s)_{o d d} = d$ has the $1 \times 1$ matrix $u$ in the displayed bases and $τ (C_{∙}) = [u]$ by [F1] and [F2]. If $q$ is even then $C_{o d d} = C_{q - 1}$ , $C_{e v e n} = C_{q}$ and $d$ vanishes on $C_{q - 1}$ , so $(d + s)_{o d d} = s$ has the $1 \times 1$ matrix $u^{- 1}$ and $τ (C_{∙}) = [u^{- 1}] = - [u]$ by [F3]. This proves assertions 1 and 2, with the single formula $τ (C_{∙}) = (- 1)^{q + 1} [u]$ .

F1F2F3

2.1

For $R = Z [π]$ , apply the quotient homomorphism $K_{1} (R) \to W h (π)$ to the torsion class $(- 1)^{q + 1} [u]$ computed in step 1.2. Its image is $(- 1)^{q + 1}$ times the image of $[u]$ , which proves the same formula in the Whitehead group.

F3step 1.2∎

Depends on

Used by

Ordinary acyclicity forgets nonzero group-ring torsion Counterexample

Dependency tree · two levels

16 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

Lück, §2.2, equation (2.7), pp.27–28 (standard reference, not scraped)
Cohen, §19, pp.62–65 (standard reference, not scraped)