Prove2Me

Theorem 4.10: FF is not elementary amenable

Proved
CannonFloydParry.not_elementaryAmenable_F

by dbenbenn · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

amenabilitygroup-theorypiecewise-linearthompsons-group

Thompson's group FF does not belong to the class of elementary amenable groups, as defined in the bundle Chou_ElementaryAmenable: the smallest class containing all finite and all abelian groups and closed under isomorphism, subgroups, quotients, extensions and directed unions. The class is taken within the universe of sets that contains FF itself (so the groups and index sets appearing in a derivation are all sets of that size); no derivation of that kind places FF in the class.

Preamble
import Definitions.Def_CannonFloydParry
import Definitions.Def_Chou_ElementaryAmenable
import Mathlib
Formal statement
namespace CannonFloydParry

/-- Theorem 4.10.  Thompson's group `F` is not elementary amenable. -/
theorem not_elementaryAmenable_F : ¬ Chou.ElementaryAmenable F := by
  sorry

end CannonFloydParry
Source
Cannon, J. W., Floyd, W. J., Parry, W. R., Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, https://doi.org/10.5169/seals-87877, Theorem 4.10, p. 233; the class is Chou's, Illinois J. Math. 24 (1980), p. 396.
Human review

  • Endorsed by Shuze Chen · Sep 19, 2026

  • Endorsed by dbenbenn · Sep 19, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph