TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 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, 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.1

Choose word metrics on $G$ and $H$ , quasi-inverse quasi-isometries $q : G \to H$ and $r : H \to G$ , and constants $λ \geq 1, c, D_{G}, D_{H} \geq 0$ such that both maps satisfy the $(λ, c)$ upper distance bound, $d_{G} (r q (x), x) \leq D_{G}$ , and $d_{H} (q r (y), y) \leq D_{H}$ . A fiber of $q$ has uniformly bounded cardinality: if $q (x) = q (x^{'})$ , the lower quasi-isometry inequality bounds $d_{G} (x, x^{'})$ , and a word-metric ball of fixed radius is finite. Let $M_{q}$ bound those fibers, and define $M_{r}$ similarly.

givenchoose

2.1

Assume $G$ is amenable. Let $E \subseteq H$ be finite and let $ε > 0$ . Put $L = \max {∣ e ∣ : e \in E}$ , taking $L = 0$ when $E = \emptyset$ , set $R = λ (L + D_{H}) + c + D_{G}$ , and let $T$ be the finite radius- $R$ ball in $G$ . Set $δ = ε / (2 M_{q} M_{r} (∣ T ∣ + 1))$ . By [L2], choose a finite nonempty $A \subseteq G$ with $∣ t A △ A ∣ < δ ∣ A ∣$ for every $t \in T$ .

L2step 1.1choose

3.1

Put $B = N_{D_{H}} (q (A))$ . It is finite and nonempty, and $∣ B ∣ \geq ∣ q (A) ∣ \geq ∣ A ∣ / M_{q}$ . If $y \in N_{L} (B) ∖ B$ , choose $b \in B$ and $a \in A$ with $d_{H} (y, b) \leq L$ and $d_{H} (b, q (a)) \leq D_{H}$ . Then $d_{G} (r (y), a) \leq R$ . Moreover $r (y) \notin A$ , since otherwise $d_{H} (y, q (r (y))) \leq D_{H}$ would put $y$ in $B$ . Hence $r (N_{L} (B) ∖ B) \subseteq N_{R} (A) ∖ A$ , and the fiber bound for $r$ gives $∣ N_{L} (B) ∖ B ∣ \leq M_{r} ∣ N_{R} (A) ∖ A ∣$ .

step 1.1step 2.1algebra

4.1

Since $N_{R} (A) ∖ A \subseteq ⋃_{t \in T} (t A ∖ A)$ , step 2.1 gives $∣ N_{R} (A) ∖ A ∣ < ∣ T ∣ δ ∣ A ∣$ . For $e \in E$ , one has $e B ∖ B \subseteq N_{L} (B) ∖ B$ and $∣ e B △ B ∣ = 2 ∣ e B ∖ B ∣$ . Combining this with step 3.1 and $∣ B ∣ \geq ∣ A ∣ / M_{q}$ yields $∣ e B △ B ∣ / ∣ B ∣ < 2 M_{q} M_{r} ∣ T ∣ δ < ε$ . Thus $B$ is an $(E, ε)$ -Folner set in $H$ .

step 2.1step 3.1algebra

5.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].

L1L2step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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