CounterexampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

$2 Z$ has index $2$ in $Z$ and is nevertheless equinumerous with $Z$

Statement refuted

If a proper subgroup $H < G$ has finite index, then $H$ cannot be equinumerous with $G$ .

Facts & Assumptions

Given: The additive group $Z$ and its subgroup $2 Z$ .

[F1]

The set $2 Z$ is a subgroup of $(Z, +)$ (Every subgroup of $(Z, +)$ is $⟨ n ⟩ = n Z$ for exactly one natural number $n$ , The integers form a commutative ring).

[F2]

The index is the number of cosets, additive cosets have the form $a + 2 Z$ , and at modulus $2$ every congruence class has exactly one representative $r$ with $0 \leq r < 2$ , hence representative $0$ or $1$ (The coset set $G / H$ and the index $[G : H]$ of a subgroup, Left and right cosets $g H$ and $H g$ of a subgroup, For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ ).

[F3]

Two sets are equinumerous when a bijection between them exists (Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection).

[F4]

Multiplication by a nonzero integer can be cancelled: if $x z = y z$ and $z \neq 0$ , then $x = y$ (The integers have no zero divisors; multiplicative cancellation).

Counterexample

technique · direct

1.1

The two cosets are $2 Z$ and $1 + 2 Z$ . Indeed [F2] writes every integer as $a = 2 q + r$ with $r \in {0, 1}$ ; then $a + 2 Z = r + 2 Z$ , since $a + 2 k = r + 2 (q + k)$ and, conversely, $r + 2 t = a + 2 (t - q)$ . Thus every coset is one of the displayed two, and they are distinct because one contains $0$ while the other does not. Hence $[Z : 2 Z] = 2$ .

F1F2

1.2

The map $f : Z \to 2 Z$ given by $f (k) = 2 k$ is surjective by the definition of $2 Z$ and injective because $2 k = 2 ℓ$ implies $k = ℓ$ by cancellation at the nonzero factor $2$ . Hence it is a bijection.

F3F4construct

2.1

Thus the proper subgroup $2 Z$ has finite index and is equinumerous with $Z$ , refuting the statement.

step 1.1step 1.2F1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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

Thomas W. Judson, Abstract Algebra: Theory and Applications, Cosets and Lagrange's Theorem (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §6.1: Cosets (standard reference, not scraped)

2Z2Z has index 22 in ZZ and is nevertheless equinumerous with ZZ