Alphabeta Math
False statementConstruction: AI-adaptedVerification: 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.

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

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.

L2L4givenchoose
2.1

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.

L1L3step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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