CorollaryStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

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.1

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.

L1L4L5given

1.2

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$ .

L2L3L4given

2.1

Steps 1.1 and 1.2 prove the two claims.

step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

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