Alphabeta Math
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.

✓ 20 results · all verified · 8 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 12 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Amenable Groups and Folner Criteria

1 · Prerequisites

2 · Summary

This page treats amenability through three linked lenses: invariant means, Folner sets, and paradoxical decompositions. The early permanence results are proved without hiding them inside Tarski's theorem, and the steps that pass from Folner or paradoxical data back to invariant means record their ultrafilter and matching-extension costs explicitly.

The landmark theorem is the Folner criterion. After that, the page extracts Folner sequences in the countable case, derives amenability from subexponential growth, and then turns to paradoxical decompositions and the nonamenability of the rank-two free group. The closing theorem records that, for finitely generated groups, amenability depends only on quasi-isometry type.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Means on bounded functions on a group

Definition

Let G be a group. Write ℓ∞(G) for the real vector space of bounded functions f:G→R.

A mean on ℓ∞(G) is a linear map

m:ℓ∞(G)→R

such that:

  1. f≥0 pointwise implies m(f)≥0;
  2. m(1G)=1, where 1G is the constant function 1.

Positivity and normalization imply ∣m(f)∣≤∥f∥∞, so a mean is automatically bounded of norm 1.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Left translation on bounded functions

Definition

Let G be a group and f∈ℓ∞(G). For g∈G, the left translate of f by g is the bounded function

(g⋅f)(x):=f(g−1x)(x∈G).

This defines a left action of G on ℓ∞(G) because e⋅f=f and (gh)⋅f=g⋅(h⋅f).

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Left-invariant means and amenable groups

Definition

A mean m on ℓ∞(G) is left invariant if

m(g⋅f)=m(f)for all g∈G, f∈ℓ∞(G).

The group G is amenable if it admits a left-invariant mean on ℓ∞(G).

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Left and right amenability agree by inversion

Statement

Let G be a group. Then G admits a left-invariant mean if and only if it admits a right-invariant mean.

Here a mean m is right invariant when m(f⋅g)=m(f) for every g∈G, where (f⋅g)(x)=f(xg−1).

Facts & Assumptions

Given: A group G.

[L1]

Amenability is defined by existence of a left-invariant mean (Left-invariant means and amenable groups).

Proof

technique · direct
1.1L1givenconstruct

Suppose m is left invariant. For bounded f, define If(x)=f(x−1) and mr(f)=m(If). Then mr is a mean, and for every g∈G one has I(f⋅g)=g−1⋅If, so left invariance of m gives mr(f⋅g)=mr(f). Thus a left-invariant mean produces a right-invariant mean.

2.1step 1.1∎

Replacing g by g−1 in the same computation shows that inversion also carries right-invariant means back to left-invariant means. Hence the two notions are equivalent.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Finite groups are amenable

Statement

Every finite group is amenable.

Facts & Assumptions

Given: A finite group G.

[L1]

A group is amenable exactly when it admits a left-invariant mean (Left-invariant means and amenable groups).

Proof

technique · direct
1.1givenconstruct

Define m(f)=∣G∣−1∑x∈Gf(x) on ℓ∞(G). This is linear, positive, and satisfies m(1G)=1, so it is a mean.

2.1L1step 1.1algebra∎

For every g∈G, the map x↦g−1x is a permutation of G, so ∑x∈Gf(g−1x)=∑x∈Gf(x). Therefore m(g⋅f)=m(f), and [L1] makes G amenable.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Folner sets and the Folner condition

Definition

Let G be a group, let S⊆G be finite, and let ε>0. A finite nonempty subset F⊆G is an (S,ε)-Folner set if

∣sF△F∣<ε∣F∣for every s∈S.

The group G satisfies the Folner condition if for every finite S⊆G and every ε>0 there exists an (S,ε)-Folner set.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Equivalent boundary formulations of the Folner condition

Statement

Let G be a group, S⊆G finite, and F⊆G finite nonempty. Then:

  1. ∣sF△F∣<ε∣F∣ for every s∈S if and only if ∣sF∖F∣<(ε/2)∣F∣ for every s∈S.
  2. Replacing the left translates sF by right translates Fs gives an equivalent condition after inversion.

Facts & Assumptions

Given: A group G, a finite subset S⊆G, a finite nonempty set F⊆G, and a real ε>0.

[L1]

An (S,ε)-Folner set is defined by the symmetric-difference inequality (Folner sets and the Folner condition).

Proof

technique · direct
1.1L1givenalgebra

For each s∈S, left translation by s is a bijection of G, so ∣sF∣=∣F∣ and therefore ∣sF△F∣=∣sF∖F∣+∣F∖sF∣=2∣sF∖F∣. Hence the symmetric-difference and one-sided boundary formulations differ only by the factor 2.

2.1step 1.1givenalgebra∎

Inversion is a bijection F↦F−1 with ∣(sF)△F∣=∣(F−1s−1)△F−1∣. Thus the left-translate and right-translate versions are equivalent after replacing S by S−1.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma, the Folner condition is equivalent to amenability

Statement

Assume the ultrafilter lemma. A group G is amenable if and only if it satisfies the Folner condition.

The proof spends the ultrafilter extension twice: first to take a limit of finite averages, and then to extend compatible finite Hall matchings when proving the reverse implication by contradiction.

Facts & Assumptions

Given: A group G and the ultrafilter lemma.

[A1]

Under the ultrafilter lemma, every proper filter extends to an ultrafilter (The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter).

[L1]

Amenability means existence of a left-invariant mean (Left-invariant means and amenable groups).

[L2]

The Folner condition asks for finite nonempty sets with arbitrarily small boundary under each finite test set (Folner sets and the Folner condition).

[L3]

One may replace symmetric differences by one-sided boundaries up to a fixed factor (Equivalent boundary formulations of the Folner condition).

[L4]

Hall's theorem gives a matching saturating the finite left part of a finite bipartite graph exactly when every subset of that left part has enough neighbours (Hall's marriage theorem for a finite bipartite graph).

Proof

technique · direct
1.1A1L1L2L3givenconstruct

Assume G satisfies the Folner condition. Let D be the directed set of triples (S,n,F) with S⊆G finite, n≥1, and F an (S,1/n)-Folner set, ordered by enlarging S and n. For d=(S,n,F), define md(f)=∣F∣−1∑x∈Ff(x). These md are means, and [L3] implies that if g∈S then ∣md(g⋅f)−md(f)∣≤∥f∥∞/n. The cofinal tails Dg,N={(S,n,F):g∈S, n≥N} have the finite intersection property, so by [A1] some ultrafilter on D contains all of them. The ultrafilter limit of the bounded family (md(f))d∈D is therefore a left-invariant mean on G.

1.2L2L3givenalgebra

Assume instead that G is amenable but not Folner. Then some finite S⊆G and ε>0 satisfy: for every finite nonempty F⊆G, some s∈S has ∣sF△F∣≥ε∣F∣. Put S0=S∪{e} and δ=ε/2. Since ∣sF∣=∣F∣, [L3] gives ∣sF∖F∣≥δ∣F∣ for that s, and hence ∣S0F∣≥(1+δ)∣F∣.

2.1step 1.2constructalgebra

Choose m≥1 with (1+δ)m≥2 and put K=S0m. Applying step 1.2 successively to F,S0F,…,S0m−1F gives ∣KF∣≥2∣F∣ for every finite nonempty F⊆G.

3.1L4step 2.1construct

Form the bipartite graph with left vertices G×{1,2}, right vertices G, and edges (g,r)∼kg for k∈K. If P is a finite set of left vertices and Q is its projection to G, then N(P)=KQ and ∣P∣≤2∣Q∣≤∣KQ∣ by step 2.1. Thus [L4] gives a matching saturating every prescribed finite left set.

4.1A1step 3.1construct

Let M be the set of finite partial matchings in this graph, and for finite P⊆G×{1,2} let XP be the set of members of M whose domains contain P. Step 3.1 shows that the family (XP) has the finite-intersection property. By [A1], an ultrafilter U on M contains every XP. For a left vertex ℓ, the set X{ℓ} is the disjoint union of the finitely many sets on which the partial matching assigns a fixed neighbour y∈N(ℓ). Exactly one such cell belongs to U; call its neighbour Φ(ℓ). If distinct left vertices had the same Φ-value, the two corresponding cells would have empty intersection, contradicting closure of U under intersections. Hence Φ:G×{1,2}→G is injective and satisfies Φ(g,r)∈Kg.

5.1L1step 4.1algebracontradiction

Write Φr(g)=Φ(g,r) and, for r∈{1,2} and k∈K, put Dr,k={g:Φr(g)=kg}. For each fixed r, the sets Dr,k partition G, while the sets kDr,k partition the range Rr of Φr; injectivity of Φ makes R1 and R2 disjoint. If mG is a left-invariant mean, write mG(E)=mG(1E). Finite additivity and invariance give mG(Rr)=∑k∈KmG(kDr,k)=∑k∈KmG(Dr,k)=mG(G)=1 for r=1,2. But R1∩R2=∅, so positivity gives 2=mG(R1)+mG(R2)=mG(R1⊔R2)≤mG(G)=1, a contradiction.

6.1step 1.1step 1.2step 5.1discharge-contradiction∎

Therefore an amenable group cannot fail the Folner condition. Together with step 1.1, this proves the equivalence.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma, abelian groups are amenable

Statement

Assume the ultrafilter lemma. Every abelian group is amenable.

Facts & Assumptions

Given: An abelian group A and the ultrafilter lemma.

[L1]

A finitely generated abelian group is isomorphic to Zr⊕T with T finite (The fundamental theorem of finitely generated abelian groups from PID modules).

[L2]

Under the ultrafilter lemma, the Folner condition is equivalent to amenability (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Proof

technique · direct
1.1L1givenalgebra

Suppose first that A is finitely generated. By [L1], write A≅Zr⊕T with T finite. Let S⊆A be finite and let ε>0. If r=0, then A=T is finite and F=A satisfies sF=F for every s∈S, so the Folner condition is immediate. Assume now that r≥1. Transport S across the isomorphism, and let M be the maximum of the ℓ∞-norms of the Zr-components of the transported elements. For n≥1, put Bn=[−n,n]r×T. Then every translate by an element of S changes only the M-thick boundary layers of the box, so ∣(s+Bn)△Bn∣=O(nr−1) uniformly in s∈S, while ∣Bn∣=(2n+1)r∣T∣. For large n this gives ∣(s+Bn)△Bn∣<ε∣Bn∣ for every s∈S. Thus finitely generated abelian groups satisfy the Folner condition.

2.1L2step 1.1

By [L2], every finitely generated abelian group is therefore amenable.

3.1L2step 2.1given∎

Now let A be arbitrary. Given a finite subset S⊆A and ε>0, the subgroup ⟨S⟩ is finitely generated and abelian, so step 2.1 makes it amenable. Applying [L2] inside ⟨S⟩ yields a finite nonempty set F⊆⟨S⟩ with ∣sF△F∣<ε∣F∣ for every s∈S. The same set F witnesses the Folner condition in A. Since S and ε were arbitrary, [L2] shows that every abelian group is amenable.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma, subgroups and quotients of amenable groups are amenable

Statement

Assume the ultrafilter lemma. Every subgroup of an amenable group is amenable, and every quotient of an amenable group by a normal subgroup is amenable.

Facts & Assumptions

Given: An amenable group G and the ultrafilter lemma.

[L1]

Amenability means existence of a left-invariant mean (Left-invariant means and amenable groups).

[L2]

Normal subgroups are the conjugation-invariant subgroups for which the quotient group is formed (Normal subgroup: invariance under conjugation).

[L3]

Under the ultrafilter lemma, amenability is equivalent to the Folner condition (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Proof

technique · direct
1.1L3givenalgebra

Let H≤G. To show that H is amenable, by [L3] it is enough to verify the Folner condition in H. Fix a finite subset S⊆H and ε>0. If S=∅, then {e}⊆H is already an (S,ε)-Folner set. Assume now that S≠∅, and put δ=ε/∣S∣. Since G is amenable, [L3] gives a finite nonempty set F⊆G with ∣sF△F∣<δ∣F∣ for every s∈S. Write F=⨆j=1mEjtj, where the Ej are the nonempty intersections of F with the finitely many right H-cosets that meet F, transported back into H. For each s∈S, left translation by s preserves every right H-coset Htj, so sF△F=⨆j=1m((sEj)tj△Ejtj) and hence ∑j=1m∣sEj△Ej∣=∣sF△F∣. Summing over s∈S gives ∑j=1m∑s∈S∣sEj△Ej∣<∣S∣δ∣F∣=ε∣F∣=ε∑j=1m∣Ej∣. Therefore some j satisfies ∑s∈S∣sEj△Ej∣<ε∣Ej∣, and then each summand is itself <ε∣Ej∣. So Ej is an (S,ε)-Folner set in H. Since S and ε were arbitrary, H satisfies the Folner condition, and [L3] makes H amenable.

1.2L1L2given

Let N⊴G, and let q:G→G/N be the quotient map from [L2]. For bounded u:G/N→R, define mG/N(u)=m(u∘q) using a left-invariant mean m on G. Then mG/N is a mean, and for gˉ=gN one has (gˉ⋅u)∘q=g⋅(u∘q), so left invariance of m implies mG/N(gˉ⋅u)=mG/N(u). Therefore the quotient is amenable.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the two permanence statements.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Extensions of amenable groups are amenable

Statement

Let N⊴G. If N and G/N are amenable, then G is amenable.

Facts & Assumptions

Given: A normal subgroup N⊴G such that both N and G/N are amenable.

[L1]

Amenability means existence of a left-invariant mean (Left-invariant means and amenable groups).

[L2]

Quotients are formed from normal subgroups (Normal subgroup: invariance under conjugation).

Proof

technique · direct
1.1L1L2givenconstruct

Let mN be a left-invariant mean on N. For bounded f:G→R and g∈G, define Φf(gN):=mN(n↦f(gn)). If g′=gh with h∈N, then the integrand for g′ is n↦f(ghn), which is the left translate of n↦f(gn) by h−1 in the N-variable. Thus the value of Φf(gN) does not depend on the chosen representative of the right coset gN. The same formula also shows ∣Φf(gN)∣≤∥f∥∞, so Φf is bounded on G/N.

2.1L1step 1.1

Let mQ be a left-invariant mean on G/N, and set mG(f)=mQ(Φf). Positivity and mG(1G)=1 are immediate. For x∈G, one has Φx⋅f(gN)=mN(n↦f(x−1gn))=Φf(x−1gN), so Φx⋅f=xN⋅Φf. Therefore mG(x⋅f)=mQ(xN⋅Φf)=mQ(Φf)=mG(f).

3.1L1step 2.1∎

Thus mG is a left-invariant mean on G, so [L1] makes G amenable.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Locally finite groups

Definition

A group G is locally finite if every finitely generated subgroup of G is finite.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Under the ultrafilter lemma, directed unions of amenable subgroups are amenable

Statement

Assume the ultrafilter lemma. Let G=⋃i∈IHi be a directed union of subgroups. If every Hi is amenable, then G is amenable.

Facts & Assumptions

Given: A directed family of amenable subgroups (Hi)i∈I whose union is G, and the ultrafilter lemma.

[L1]

Under the ultrafilter lemma, amenability is equivalent to the Folner condition (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Proof

technique · direct
1.1L1givenchoose

Let S⊆G be finite and let ε>0. Because the family is directed and ⋃iHi=G, some index i satisfies S⊆Hi. Since Hi is amenable, [L1] gives a finite nonempty set F⊆Hi with ∣sF△F∣<ε∣F∣ for every s∈S.

2.1L1step 1.1∎

The set F from step 1.1 is also an (S,ε)-Folner set when viewed inside G. Since S and ε were arbitrary, G satisfies the Folner condition. Therefore [L1] makes G amenable.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma, solvable groups and locally finite groups are amenable

Statement

Assume the ultrafilter lemma. Every solvable group is amenable, and every locally finite group is amenable.

Facts & Assumptions

Given: A solvable group or a locally finite group, and the ultrafilter lemma.

[L1]

Solvability is defined by the derived series terminating at the trivial group (The derived series, solvable groups, and derived length).

[L2]

A group is locally finite when every finitely generated subgroup is finite (Locally finite groups).

[L3]

Directed unions of amenable subgroups are amenable (Under the ultrafilter lemma, directed unions of amenable subgroups are amenable).

[L4]

Finite groups are amenable, and under the ultrafilter lemma so are abelian groups (Finite groups are amenable, Under the ultrafilter lemma, abelian groups are amenable).

[L5]

Extensions of amenable groups are amenable (Extensions of amenable groups are amenable).

Proof

technique · direct
1.1L1L4L5given

Let G be solvable. If its derived length is 0, then G is trivial and hence finite, so [L4] applies. If the derived length is positive, then G′=[G,G] has smaller derived length by [L1], and the quotient G/G′ is abelian. Inducting on derived length and applying [L5] shows that every solvable group is amenable.

1.2L2L3L4given

Let G be locally finite. The family of finitely generated subgroups of G is directed by inclusion, its union is all of G, and every member is finite by [L2]. Hence each member is amenable by [L4], and [L3] gives amenability of G.

2.1step 1.1step 1.2∎

Steps 1.1 and 1.2 prove the two claims.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-28Open item page →

Folner sequences for enumerated groups

Definition

Let G={g1,g2,… } be an enumerated countable group. A sequence (Fn)n≥1 of finite nonempty subsets of G is a Folner sequence if

lim⁡n→∞∣giFn△Fn∣∣Fn∣=0for every fixed i≥1.

Equivalently, for every finite subset S⊆G and every ε>0, all sufficiently large Fn are (S,ε)-Folner sets.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Enumerated countable amenable groups admit Folner sequences

Statement

Let G={g1,g2,… } be an enumerated countable amenable group. Then G admits a Folner sequence.

Facts & Assumptions

Given: An enumerated countable amenable group G={g1,g2,… }.

[L1]

A Folner sequence is a sequence of finite nonempty sets with vanishing relative symmetric-difference error for each fixed group element (Folner sequences for enumerated groups).

[L2]

Every amenable group satisfies the Folner condition (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Proof

technique · direct
1.1L2givenchoose

For each n≥1, apply [L2] to the finite test set Sn={g1,…,gn} and the tolerance 1/n. This gives a finite nonempty set Fn⊆G with ∣giFn△Fn∣<∣Fn∣/n for every i≤n.

2.1L1step 1.1∎

Fix i. Once n≥i, step 1.1 gives ∣giFn△Fn∣/∣Fn∣<1/n, which tends to 0. Therefore (Fn) is a Folner sequence in the sense of [L1].

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma, subexponential growth implies amenability

Statement

Assume the ultrafilter lemma. Every finitely generated group of subexponential growth is amenable.

Facts & Assumptions

Given: A finitely generated group G with a finite generating set S, subexponential growth, and the ultrafilter lemma.

[L1]

The growth function counts word-metric balls (The growth function of a finitely generated group).

[L2]

Subexponential growth means that no exponential lower bound occurs (Polynomial, subexponential, exponential, and intermediate growth).

[L3]

Under the ultrafilter lemma, the Folner condition implies amenability (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Proof

technique · direct
1.1L1L2givenalgebra

Let Bn be the word-metric ball of radius n about the identity. If some δ>0 satisfied ∣SBn∣≥(1+δ)∣Bn∣ for every n, then iterating would give ∣Bn∣≥(1+δ)n up to multiplicative constants, contradicting the subexponential alternative in [L2]. Therefore for every ε>0 there exists n with ∣SBn∖Bn∣<(ε/2)∣Bn∣.

2.1L3step 1.1algebra∎

For such an n, every s∈S satisfies ∣sBn∖Bn∣≤∣SBn∖Bn∣<(ε/2)∣Bn∣, so the boundary formulation of [L3] makes Bn an (S,ε)-Folner set. Hence G satisfies the Folner condition, and [L3] shows that G is amenable.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Paradoxical decompositions of groups

Definition

Let G be a group. A paradoxical decomposition of G consists of pairwise disjoint subsets

A1,…,Am, B1,…,Bn⊆G

and group elements a1,…,am,b1,…,bn∈G such that

G=⨆i=1mAi⊔⨆j=1nBj=⨆i=1maiAi=⨆j=1nbjBj.

Thus the group is partitioned into finitely many pieces, and each of the two subfamilies can be translated to cover the whole group again.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Paradoxical groups admit no invariant mean

Statement

If a group admits a paradoxical decomposition, then it admits no left-invariant mean.

Facts & Assumptions

Given: A group G with a paradoxical decomposition.

[L1]

A left-invariant mean is a positive normalized functional on ℓ∞(G) invariant under left translation (Left-invariant means and amenable groups).

[L2]

In a paradoxical decomposition, disjoint pieces Ai,Bj partition G, and the translated families (aiAi) and (bjBj) each partition G (Paradoxical decompositions of groups).

Proof

technique · direct
1.1L1L2givenassume-contra

Assume toward contradiction that m is a left-invariant mean on G. By [L2] and positivity, finite additivity on indicator functions gives 1=m(1G)=∑im(1Ai)+∑jm(1Bj).

2.1L1L2step 1.1discharge-contradiction∎

The translated families from [L2] also partition G, so left invariance gives 1=m(1G)=∑im(1aiAi)=∑im(1Ai) and likewise 1=∑jm(1Bj). Combining these equalities with step 1.1 yields 1=2, a contradiction.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma and a matching-extension principle, a group is amenable if and only if it is not paradoxical

Statement

Assume the ultrafilter lemma and the following perfect-matching extension principle for G: whenever a finite set K⊆G satisfies ∣KF∣≥2∣F∣ for every finite nonempty F⊆G, the finite Hall matchings in the bipartite graph with left vertices G×{1,2}, right vertices G, and edges (g,r)∼kg for k∈K extend to a bijection Φ:G×{1,2}→G satisfying Φ(g,r)∈Kg.

Under these assumptions, G is amenable if and only if it is not paradoxical.

Facts & Assumptions

Given: A group G, the ultrafilter lemma, and the matching-extension principle stated above.

[L1]

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

[A1]

Under the ultrafilter lemma, amenability is equivalent to the Folner condition (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

[A2]

The perfect-matching extension principle above upgrades the finite Hall matchings coming from a doubling set K to an edge-respecting bijection G×{1,2}→G.

[L2]

Hall's theorem saturates a finite bipartite left part exactly when every finite subfamily has enough neighbors (Hall's marriage theorem for a finite bipartite graph).

Proof

technique · direct
1.1L1given

If G is paradoxical, then [L1] says that no left-invariant mean exists, so G is not amenable. This proves the forward implication of the statement.

1.2A1givenalgebra

Assume now that G is not amenable. By contrapositive use of [A1], there is a finite set K⊆G with e∈K such that ∣KF∣≥2∣F∣ for every finite nonempty F⊆G. Indeed, if no such K existed, then for a finite test set S and ε>0 one could put S0={e}∪S∪S−1, choose m with (1+ε/2)m>2, and find finite nonempty F with ∣S0mF∣<2∣F∣. Among the layers Fj=S0jF, some ratio ∣Fj+1∣/∣Fj∣ would then be below 1+ε/2, giving ∣sFj△Fj∣<ε∣Fj∣ for every s∈S and hence the Folner condition.

2.1A2L2step 1.2construct

Form the bipartite graph from [A2]. For every finite left subset P⊆G×{1,2} with projection Q⊆G, step 1.2 gives ∣N(P)∣=∣KQ∣≥2∣Q∣≥∣P∣, so [L2] produces a matching saturating P. By [A2], these finite matchings extend to an edge-respecting bijection Φ:G×{1,2}→G. For r∈{1,2} and k∈K, put Cr,k={Φ(g,r):Φ(g,r)=kg}. The finitely many Cr,k are pairwise disjoint and partition G because Φ is bijective. For fixed r, the translated pieces k−1Cr,k partition G, because they are exactly the fibers in the domain copy G×{r}. Thus the two subfamilies (C1,k)k∈K and (C2,k)k∈K, with translators k−1, form a paradoxical decomposition.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove both directions, so G is amenable exactly when it is not paradoxical.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

The free group of rank two is nonamenable

Statement

The free group of rank two is nonamenable.

Facts & Assumptions

Given: The free group F2 of rank two.

[L1]

F2 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 F2=⟨a,b⟩. For x∈{a,a−1,b,b−1}, let W(x) be the set of nonempty reduced words whose first letter is x. Put P={an:n≥0} and P+={an:n≥1}, and define A1=W(a)∖P+, A2=W(a−1)∪P, B1=W(b), and B2=W(b−1).

2.1step 1.1algebra

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

3.1L3step 1.1step 2.1algebra

Left multiplication gives aW(a−1)=F2∖W(a) and aP=P+, hence F2=A1⊔aA2. Likewise bW(b−1)=F2∖W(b), hence F2=B1⊔bB2. 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 F2, so [L2] implies that F2 admits no left-invariant mean and is therefore nonamenable.

CorollaryStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28Open item page →

Under the ultrafilter lemma, groups containing a rank-two free subgroup are nonamenable

Statement

Assume the ultrafilter lemma. If a group contains a free subgroup of rank 2, then it is nonamenable.

Facts & Assumptions

Given: A group G containing a subgroup H≅F2, and the ultrafilter lemma.

[L1]

The rank-two free group is nonamenable (The free group of rank two is nonamenable).

[L2]

Under the ultrafilter lemma, subgroups of amenable groups are amenable (Under the ultrafilter lemma, subgroups and quotients of amenable groups are amenable).

Proof

technique · direct
1.1L2givenassume-contra

If G were amenable, then [L2] would make its subgroup H amenable.

2.1L1step 1.1discharge-contradiction∎

But H≅F2, and [L1] says F2 is nonamenable. This contradiction proves that G is nonamenable.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

Under the ultrafilter lemma, amenability is a quasi-isometry invariant for finitely generated groups

Statement

Assume the ultrafilter lemma. Amenability is a quasi-isometry invariant of finitely generated groups.

Facts & Assumptions

Given: Two finitely generated quasi-isometric groups G and H, and the ultrafilter lemma.

[L1]

A property of finitely generated groups is a quasi-isometry invariant when it depends only on quasi-isometry type (Quasi-isometry invariants and geometric properties of finitely generated groups).

[L2]

Under the ultrafilter lemma, amenability is equivalent to the Folner condition (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Proof

technique · direct
1.1givenchoose

Choose word metrics on G and H, quasi-inverse quasi-isometries q:G→H and r:H→G, and constants λ≥1,c,DG,DH≥0 such that both maps satisfy the (λ,c) upper distance bound, dG(rq(x),x)≤DG, and dH(qr(y),y)≤DH. A fiber of q has uniformly bounded cardinality: if q(x)=q(x′), the lower quasi-isometry inequality bounds dG(x,x′), and a word-metric ball of fixed radius is finite. Let Mq bound those fibers, and define Mr similarly.

2.1L2step 1.1choose

Assume G is amenable. Let E⊆H be finite and let ε>0. Put L=max⁡{∣e∣:e∈E}, taking L=0 when E=∅, set R=λ(L+DH)+c+DG, and let T be the finite radius-R ball in G. Set δ=ε/(2MqMr(∣T∣+1)). By [L2], choose a finite nonempty A⊆G with ∣tA△A∣<δ∣A∣ for every t∈T.

3.1step 1.1step 2.1algebra

Put B=NDH(q(A)). It is finite and nonempty, and ∣B∣≥∣q(A)∣≥∣A∣/Mq. If y∈NL(B)∖B, choose b∈B and a∈A with dH(y,b)≤L and dH(b,q(a))≤DH. Then dG(r(y),a)≤R. Moreover r(y)∉A, since otherwise dH(y,q(r(y)))≤DH would put y in B. Hence r(NL(B)∖B)⊆NR(A)∖A, and the fiber bound for r gives ∣NL(B)∖B∣≤Mr∣NR(A)∖A∣.

4.1step 2.1step 3.1algebra

Since NR(A)∖A⊆⋃t∈T(tA∖A), step 2.1 gives ∣NR(A)∖A∣<∣T∣δ∣A∣. For e∈E, one has eB∖B⊆NL(B)∖B and ∣eB△B∣=2∣eB∖B∣. Combining this with step 3.1 and ∣B∣≥∣A∣/Mq yields ∣eB△B∣/∣B∣<2MqMr∣T∣δ<ε. Thus B is an (E,ε)-Folner set in H.

5.1L1L2step 4.1∎

Since E and ε were arbitrary, step 4.1 gives the Folner condition in H, so [L2] makes H amenable. Applying the same argument to the quasi-inverse transfers amenability from H to G. Therefore amenability depends only on quasi-isometry type, as asserted in [L1].

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

FALSE: amenable means finite

Statement

Every amenable group is finite.

Facts & Assumptions

Given: The false claim above and the ultrafilter lemma.

[L1]

Under the ultrafilter lemma, every abelian group is amenable (Under the ultrafilter lemma, abelian groups are amenable).

Refutation

technique · direct
1.1given

The additive group (Z,+) is abelian and infinite.

2.1L1step 1.1∎

By [L1], (Z,+) is amenable. Since it is infinite, it refutes the statement.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-28Open item page →

FALSE: one finite Folner set proves amenability

Statement

The existence of one finite Folner set is enough to prove that a group is amenable.

Facts & Assumptions

Given: The false claim above.

[L1]

The Folner condition requires the inequalities over every finite test set and every tolerance; under the ultrafilter lemma it is equivalent to amenability (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

Refutation

technique · direct
1.1givenconstruct

Let G=F2, which is nonamenable. The singleton {e} satisfies ∣e{e}△{e}∣=0, so it is a ({e},1)-Folner set.

2.1L1step 1.1∎

This single accidental Folner set does not make G amenable, because [L1] requires the inequalities for all finite test sets and arbitrarily small tolerances. Therefore the statement is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-28Open item page →

FALSE: every uncountable amenable group has a Folner sequence

Statement

Every uncountable amenable group admits a global Folner sequence, meaning a sequence (Fn)n∈N of finite nonempty subsets such that ∣gFn△Fn∣∣Fn∣⟶0 for every g in the group. This is the natural extension of the countable definition to a group for which no enumeration is available.

Facts & Assumptions

Given: The false claim above and the ultrafilter lemma.

[L1]

For an enumerated countable group, a Folner sequence is indexed by the natural numbers and is almost invariant under each fixed group element (Folner sequences for enumerated groups); the Statement explicitly extends that same pointwise condition to arbitrary groups.

[L2]

Under the ultrafilter lemma, abelian groups are amenable (Under the ultrafilter lemma, abelian groups are amenable).

[L3]

The Folner criterion is a finite-test condition, not a countable-sequence statement for uncountable groups (Under the ultrafilter lemma, the Folner condition is equivalent to amenability).

[L4]

The ordered additive group R is uncountable (R is uncountable (Cantor's nested intervals, 1874)).

Refutation

technique · direct
1.1L2L4givenchoose

Let G=(R,+). It is abelian and therefore amenable by [L2], and it is uncountable by [L4]. Let (Fn) be any sequence of finite nonempty subsets of G, and put A=⋃n(Fn−Fn). Each finite subset of the ordered set R has a unique increasing enumeration, so the sets Fn−Fn can be enumerated canonically and A is at most countable. By [L4], choose g∈R∖A.

2.1L1L3step 1.1algebra∎

For this g, one has (g+Fn)∩Fn=∅ for every n, since an intersection would put g in Fn−Fn⊆A. Hence ∣(g+Fn)△Fn∣=2∣Fn∣ and the ratio in [L1] is always 2, never 0. Thus (Fn) is not a global Folner sequence. The amenability from step 1.1 does not force a contradiction, because [L3] is only a finite-test criterion and does not supply one countable family for all elements of an uncountable group. Since the sequence was arbitrary, the statement is false.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28Open item page →

FALSE: a paradoxical decomposition is just an abstract partition without prescribed translates

Statement

A paradoxical decomposition is nothing more than a set-theoretic partition of a group.

Facts & Assumptions

Given: The false claim above.

[L1]

A paradoxical decomposition includes specified translating group elements and translated copies covering the whole group (Paradoxical decompositions of groups).

Refutation

technique · direct
1.1givenconstruct

Partition (Z,+) into the even integers and the odd integers. This is an ordinary set-theoretic partition.

2.1L1step 1.1∎

By [L1], a paradoxical decomposition needs finitely many specified translates whose images each cover the whole group again. The even/odd partition by itself carries no such data, so it is not a paradoxical decomposition. Thus the statement is false.

Sources