Alphabeta Math
TheoremStatement: 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, 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 ZrT 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.1

Suppose first that A is finitely generated. By [L1], write AZrT with T finite. Let SA be finite and let ε>0. If r=0, then A=T is finite and F=A satisfies sF=F for every sS, so the Folner condition is immediate. Assume now that r1. Transport S across the isomorphism, and let M be the maximum of the -norms of the Zr-components of the transported elements. For n1, 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(nr1) uniformly in sS, while Bn=(2n+1)rT. For large n this gives (s+Bn)Bn<εBn for every sS. Thus finitely generated abelian groups satisfy the Folner condition.

L1givenalgebra
2.1

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

L2step 1.1
3.1

Now let A be arbitrary. Given a finite subset SA 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 FS with sFF<εF for every sS. The same set F witnesses the Folner condition in A. Since S and ε were arbitrary, [L2] shows that every abelian group is amenable.

L2step 2.1given

Depends on

Used by

Dependency tree · two levels

15 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