TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28

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 free group of rank two is nonamenable

Statement

The free group of rank two is nonamenable.

Facts & Assumptions

Given: The free group $F_{2}$ of rank two.

[L1]

$F_{2}$ is the free group on two generators, say $a$ and $b$ (The free product of two infinite cyclic groups is the free group on two generators).

[L2]

A paradoxical decomposition forbids a left-invariant mean (Paradoxical groups admit no invariant mean).

[L3]

Paradoxical decompositions are defined by finitely many translated pieces (Paradoxical decompositions of groups).

Proof

technique · direct

1.1L1L3givenconstruct

By [L1], write $F_{2} = ⟨ a, b ⟩$ . For $x \in {a, a^{- 1}, b, b^{- 1}}$ , let $W (x)$ be the set of nonempty reduced words whose first letter is $x$ . Put $P = {a^{n} : n \geq 0}$ and $P_{+} = {a^{n} : n \geq 1}$ , and define $A_{1} = W (a) ∖ P_{+}$ , $A_{2} = W (a^{- 1}) \cup P$ , $B_{1} = W (b)$ , and $B_{2} = W (b^{- 1})$ .

2.1step 1.1algebra

The four sets are pairwise disjoint and partition $F_{2}$ : the usual five first-letter classes partition $F_{2}$ , and $P_{+}$ has merely been moved from $W (a)$ into the piece containing the identity.

3.1L3step 1.1step 2.1algebra

Left multiplication gives $a W (a^{- 1}) = F_{2} ∖ W (a)$ and $a P = P_{+}$ , hence $F_{2} = A_{1} ⊔ a A_{2}$ . Likewise $b W (b^{- 1}) = F_{2} ∖ W (b)$ , hence $F_{2} = B_{1} ⊔ b B_{2}$ . Thus the pieces of step 1.1, with translators $e, a, e, b$ , satisfy both partition equalities in [L3].

4.1L2step 1.1step 2.1step 3.1∎

Steps 1.1-3.1 give a paradoxical decomposition of $F_{2}$ , so [L2] implies that $F_{2}$ admits no left-invariant mean and is therefore nonamenable.

Depends on

Used by

Under the ultrafilter lemma, groups containing a rank-two free subgroup are nonamenable Corollary
The free group on two generators is not amenable Counterexample
A paradoxical decomposition of a free group of rank two Example
Boundary expansion in the free group Example

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

C. Löh, Geometric Group Theory: An Introduction (2015 course version) (standard reference, not scraped)
Cornelia Drutu and Michael Kapovich, Lectures on Geometric Group Theory (standard reference, not scraped)