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.

A vanishing group-ring coefficient sum pairs off opposite-signed equal labels

Statement

Let $π$ be a group and let $g_{1}, \dots, g_{r} \in π$ and $ε_{1}, \dots, ε_{r} \in {\pm 1}$ satisfy $\sum_{j = 1}^{r} ε_{j} [g_{j}] = 0$ in $Z [π]$ , or $\sum_{j = 1}^{r} ε_{j} [g_{j}] = [h]$ for a single element $h \in π$ . If $r \geq 2$ , then there are indices $j_{1} \neq j_{2}$ with $g_{j_{1}} = g_{j_{2}}$ and $ε_{j_{1}} = - ε_{j_{2}}$ . In particular, in the single-monomial case with $r \geq 2$ the multiset of signed labels contains an opposite-signed pair of equal labels.

Facts & Assumptions

Given: A group $π$ , a finite list $g_{1}, \dots, g_{r} \in π$ of elements and signs $ε_{1}, \dots, ε_{r} \in {\pm 1}$ , together with the equality $\sum_{j = 1}^{r} ε_{j} [g_{j}] = 0$ , or the equality $\sum_{j = 1}^{r} ε_{j} [g_{j}] = [h]$ for a single element $h \in π$ .

[F1]

The classes $[g]$ , $g \in π$ , form a $Z$ -basis of $Z [π]$ : the group ring is the free left $Z$ -module on the set $π$ , and every element of $Z [π]$ has a unique expression $\sum_{g \in F} r_{g} [g]$ with $F \subseteq π$ finite and $r_{g} \in Z$ , so two such expressions are equal if and only if they have the same coefficient at every label; in particular the expression of $0$ has every coefficient $0$ , and the expression of a single basis vector $[h]$ has coefficient $1$ at $h$ and coefficient $0$ at every other label (The group ring $R [G]$ of finitely supported formal $R$ -linear combinations of group elements, The group ring $R [G]$ is a unital $R$ -algebra with basis $G$ , and each $g \in G$ is a unit of $R [G]$ ).

Proof

1.1F1algebra

Group the terms of the sum by label: for each $g \in π$ set $k_{g} : = \sum_{j : g_{j} = g} ε_{j} \in Z$ , a finite sum that is nonzero only for the finitely many occurring labels, so that $\sum_{j = 1}^{r} ε_{j} [g_{j}] = \sum_{g \in π} k_{g} [g]$ is the expansion of the left-hand side in the basis of [F1]. By the uniqueness of that expansion, the equality $\sum_{j = 1}^{r} ε_{j} [g_{j}] = 0$ holds exactly when $k_{g} = 0$ for every $g \in π$ , and the equality $\sum_{j = 1}^{r} ε_{j} [g_{j}] = [h]$ holds exactly when $k_{h} = 1$ and $k_{g} = 0$ for every $g \neq h$ .

2.1step 1.1contradiction

Assume no two indices carry equal labels with opposite signs, so that for every occurring label $g$ all terms with $g_{j} = g$ share one sign and $k_{g}$ is $\pm$ the number of occurrences of $g$ , hence a nonzero integer. If $\sum_{j = 1}^{r} ε_{j} [g_{j}] = 0$ , then step 1.1 forces $k_{g}$ to vanish for every label, contradicting the nonzero coefficient of each occurring label; therefore in the zero-sum case some pair of indices has equal labels and opposite signs.

2.2step 1.1algebra

Assume no two indices carry equal labels with opposite signs and consider the single-monomial case $\sum_{j = 1}^{r} ε_{j} [g_{j}] = [h]$ with $r \geq 2$ . By step 1.1 every label $g \neq h$ must have $k_{g} = 0$ , and under the assumption every occurring label has a nonzero coefficient, so no label other than $h$ occurs and all $r$ terms carry the label $h$ . Then $k_{h} = \sum_{j = 1}^{r} ε_{j} = r - 2 m$ , where $m$ counts the indices with $ε_{j} = - 1$ , and the equation $k_{h} = 1$ with $r \geq 2$ gives an odd $r \geq 3$ and $1 \leq m \leq r - 1$ ; hence some index has sign $+ 1$ and some index has sign $- 1$ , both with label $h$ , so an opposite-signed pair of equal labels exists in the single-monomial case as well.

3.1step 2.1step 2.2∎

Steps 2.1 and 2.2 settle the zero-sum and the single-monomial case respectively, so under the stated hypotheses and $r \geq 2$ there are always indices $j_{1} \neq j_{2}$ with $g_{j_{1}} = g_{j_{2}}$ and $ε_{j_{1}} = - ε_{j_{2}}$ . The argument used only the basis expansion of $Z [π]$ , no property of $π$ beyond it and no choice principle.

Depends on

Used by

Dependency tree · two levels

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