Milnor: growth of finitely generated solvable groupsResearch Paper
## Motivation
This mission formalizes John Milnor's *Growth of finitely generated solvable groups*, J.
Differential Geometry 2 (1968) 447–449
([doi:10.4310/jdg/1214428659](https://doi.org/10.4310/jdg/1214428659)), a three-page addendum to
J. A. Wolf's *Growth of finitely generated solvable groups and curvature of Riemannian manifolds*,
which precedes it in the same issue (421–446,
[doi:10.4310/jdg/1214428658](https://doi.org/10.4310/jdg/1214428658)). Milnor's note has one
theorem and three lemmas, and "for definitions and explanations the reader is referred to" Wolf.
Wolf proved that a polycyclic group "either has a finitely generated nilpotent subgroup of finite
index and thus is of polynomial growth, or has no such subgroup and is of exponential growth"
(p. 421). Milnor's Theorem closes the gap between polycyclic and solvable: "Let $\Gamma$ be a
solvable group which is not polycyclic, and $S$ a finite set of generators for $\Gamma$. Then there
exists an exponential lower bound $g_S(m) \ge (\text{constant})^m > 1$ for the growth function $g_S$
of $\Gamma$." Together the two papers give the Milnor–Wolf theorem, "that a finitely generated
solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of
polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth"
(Wolf, p. 421). Milnor notes that Wolf's results "provide a partial answer to a problem which was
posed by the author in Amer. Math. Monthly 75 (1968) 685–686", and Wolf raises "the question of
whether every finitely generated group $\Gamma$, which is not of exponential growth, necessarily
has a nilpotent subgroup of finite index" (p. 422); Grigorchuk's groups of intermediate growth
([1984](https://doi.org/10.1070/IM1985v025n02ABEH001281)) later answered that in the negative,
while Gromov ([1981](https://doi.org/10.1007/BF02698687)) proved that polynomial growth does force
a nilpotent subgroup of finite index. Chou's 1980 extension of the Milnor–Wolf theorem to
elementary amenable groups, the mission
[Chou: elementary amenable groups](https://prove2.me/missions/Chou%3A%20elementary%20amenable%20groups)
on this platform, cites exactly this theorem. Wolf's paper is the subject of a companion mission.
## Setting
**Growth.** For a finite subset $S$ of a group $\Gamma$, Wolf's **growth function** $g_S(m)$ (p. 426)
is the number of elements expressible as words of length $\le m$ based on $S$, a word
$s_1^{a_1} \cdots s_r^{a_r}$ having length $|a_1| + \cdots + |a_r|$. `MilnorWolf.growthFunction S m`
takes $g_S(m)$ as the size of the ball `Chou.wordBall S m` of the published growth bundle, the set of
products of at most $m$ factors from $S \cup S^{-1}$. $\Gamma$ has
**exponential growth**, the published `Chou.HasExponentialGrowth`, if for some finite generating
set $S$ there is $c > 1$ with $g_S(m) \ge c^m$ for all $m$; Wolf shows (p. 434) that this does not
depend on $S$.
**Polycyclic groups.** Wolf's Proposition 4.1 (p. 433) gives eleven equivalent conditions; the
definition used here is condition (1): "There is a normal series
$\Gamma = A_0 \supset A_1 \supset \cdots \supset A_t = \{1\}$ with every quotient $A_i/A_{i+1}$ finite or
infinite cyclic." This is `MilnorWolf.IsPolycyclic`. A **solvable** group is
Mathlib's `Group.IsSolvable`: the derived series reaches the trivial subgroup.
**Milnor's standing assumptions.** The three lemmas concern a group extension
$1 \to A \to B \to C \to 1$ where "we will always assume that $A$ is abelian and that $B$ is
finitely generated." In the statements, $B$ is a finitely generated group, $A$ an abelian normal
subgroup, and $C$ the quotient $B/A$.
## Formalization targets
### Milnor's Theorem (p. 447)
"Let $\Gamma$ be a solvable group which is not polycyclic, and $S$ a finite set of generators for
$\Gamma$. Then there exists an exponential lower bound $g_S(m) \ge (\text{constant})^m > 1$ for
the growth function $g_S$ of $\Gamma$." Stated for an arbitrary finite generating set $S$:
$$\exists\, c > 1 \quad \forall\, m \ge 1: \qquad c^m \le g_S(m).$$
This is the goal. The constant is existentially quantified, so a sharper bound does not change
the statement. The milestones are Milnor's three lemmas,
in order, followed by one published Open theorem of the Chou mission that they prove: Chou's form
of Lemmas 1 and 2, where the normal subgroup need not be abelian.
## Significance
Milnor's Theorem is the half of the Milnor–Wolf theorem that reaches beyond polycyclic groups:
with Wolf's polycyclic dichotomy it says that a finitely generated solvable group is either almost
nilpotent, of polynomial growth, or of exponential growth, with nothing in between. That
statement is what Chou's Theorem 3.2 extends to elementary amenable groups, and it is the reason
a group of intermediate growth cannot be solvable or elementary amenable, the fact that placed
Grigorchuk's groups outside those classes.
Formalizing it produces, besides the Theorem, the three lemmas as reusable library results: the
subgroup spanned by the conjugates $\beta^k \alpha \beta^{-k}$ is finitely generated when $B$ is
not of exponential growth; a normal subgroup with finitely presented quotient is normally
generated by finitely many elements; and polycyclic-by-abelian without exponential growth is
polycyclic. The proof is complete in the paper; nothing here is open mathematics. On this
platform the Theorem and the lemmas are stated and unproved; Chou's mission holds the Open
non-abelian form of Lemmas 1 and 2 and two Open reductions that resolve once this mission and the
Wolf mission close their externals.
## Difficulty
The obvious attempt, to bound the growth of $B$ below by the growth of a free subsemigroup found
inside it, is not what Milnor does and does not obviously work for an arbitrary abelian-by-solvable
extension. Milnor's argument turns the growth hypothesis into finite generation: among the $2^m$
expressions $\beta\alpha^{i_1} \cdots \beta\alpha^{i_m}$ two must coincide, and the resulting
relation expresses $\alpha_m = \beta^m \alpha \beta^{-m}$ in terms of $\alpha_1, \ldots, \alpha_{m-1}$.
The delicate step is running this over a whole set of normal generators of $A$ and over each of
finitely many $\beta$'s in turn, so that $A$ itself comes out finitely generated (Lemma 3), and then
up the derived series of $\Gamma$. In Lean the work is in Lemma 2, which needs the finite
presentation of $C$ transported to a presentation on the images of chosen generators of $B$, and in
Lemma 3, which needs that a polycyclic group is finitely presented and that an extension of
polycyclic groups is polycyclic.
## Formalization scope
Growth is measured on the closed balls of the published bundle `Chou_Growth`: `Chou.wordBall S m`
is the set of products of at most $m$ letters from $S \cup S^{-1}$, and $g_S(m)$ is its cardinality
(a `Nat.card`, finite because $S$ is a `Finset`). "Not of exponential growth" is the negation of
the existential definition, so it is a statement about every finite generating set. Polycyclic is
Wolf's condition (1); the definition fixes the reading of "normal series". The abelian hypothesis on $A$ is Mathlib's
`IsMulCommutative` on the subgroup; finite generation and finite presentation are Mathlib's
`Group.FG` and `Group.IsFinitelyPresented`.
The Theorem's hypotheses are satisfiable: the trivial group is polycyclic, so "not polycyclic"
excludes it, and a solvable non-polycyclic finitely generated group exists (the lamplighter group
$\mathbb Z/2 \wr \mathbb Z$). No hypothesis is vacuous and no definition makes a target trivially
true.
The definitions of polycyclic group, polynomial growth and Wolf's growth exponents $E_1, E_2$ are
stated in the bundle `MilnorWolf_Growth` here because Milnor defers all definitions to Wolf; the
results of Wolf's paper, in particular the polycyclic dichotomy that combines with this Theorem
into the Milnor–Wolf theorem, belong to the companion mission. Nothing of Milnor's note is
omitted. Contributions welcome: proofs of the three lemmas and the Theorem, and general
library results they need, such as finite presentability of polycyclic groups.
## Selected references
- J. Milnor, *Growth of finitely generated solvable groups*, J. Differential Geometry 2 (1968),
447–449. [doi:10.4310/jdg/1214428659](https://doi.org/10.4310/jdg/1214428659)
- J. A. Wolf, *Growth of finitely generated solvable groups and curvature of Riemannian
manifolds*, J. Differential Geometry 2 (1968), 421–446.
[doi:10.4310/jdg/1214428658](https://doi.org/10.4310/jdg/1214428658)
- J. Milnor, *A note on curvature and fundamental group*, J. Differential Geometry 2 (1968), 1–7.
- A. G. Kurosh, *Theory of groups*, vol. II, Chelsea, 1956.
- R. I. Grigorchuk, *Degrees of growth of finitely generated groups, and the theory of invariant
means*, Math. USSR-Izv. 25 (1985), 259–300 (Russian original 1984).
[doi:10.1070/IM1985v025n02ABEH001281](https://doi.org/10.1070/IM1985v025n02ABEH001281)
- M. Gromov, *Groups of polynomial growth and expanding maps*, Publ. Math. IHÉS 53 (1981),
53–78. [doi:10.1007/BF02698687](https://doi.org/10.1007/BF02698687)
- C. Chou, *Elementary amenable groups*, Illinois J. Math. 24 (1980), 396–407 (p. 400).
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)
9 thms1 active userReviewed
🏆Completed
Captain: dbenbenn
Chou: elementary amenable groupsResearch Paper
## Motivation
Von Neumann introduced amenable groups in 1929 to explain the Hausdorff–Banach–Tarski
paradox, and showed that the class $AG$ of amenable groups contains all finite and all abelian
groups and is closed under four processes: (I) subgroups, (II) quotients, (III) extensions and
(IV) directed unions. Day named the smallest class with these properties $EG$, the
**elementary amenable** groups. For fifty years these were the only amenable groups anyone could
exhibit, and von Neumann's question whether every non-amenable group contains a free subgroup
on two generators — whether $AG$ equals the class $NF$ of groups without such a subgroup — was
open. (It was answered in the negative by Ol'shanskii in 1980, the year of this paper, by
different methods.)
Ching Chou's *Elementary amenable groups* (Illinois J. Math. 24 (1980) 396–407,
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)) gives the structure theory
of $EG$ that everything later relies on. Its central result is that the class can be built
from finite and abelian groups by extensions and directed unions *alone* — subgroups and
quotients add nothing (Proposition 2.2). From that description three things follow: periodic
elementary amenable groups are locally finite, so the periodic non-locally-finite groups of
Golod and Novikov–Adjan show $EG \subsetneq NF$ (Theorem 2.3); a finitely generated simple
elementary amenable group is finite (Corollary 2.4); and Wolf's conjecture holds in $EG$: a
finitely generated elementary amenable group is almost nilpotent or has exponential growth
(Theorem 3.2, extending Milnor and Wolf's theorem for solvable groups). A final section
introduces a packing property (P) of groups and proves it for every elementary amenable group
(Proposition 4.2) and every residually elementary amenable group (Corollary 4.7).
On this platform the definition of $EG$ is already published
(`Chou_ElementaryAmenable`, from the mission
[Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroup](https://prove2.me/missions/Cannon%E2%80%93Floyd%E2%80%93Parry%3A%20Thompson%27s%20group%20F%20and%20the%20simplicity%20of%20its%20commutator%20subgroup)),
together with the theorem that Thompson's group $F$ is not elementary amenable and, from
Brin and Squier, that $F$ has no free subgroup on two generators. This mission formalizes
Chou's paper on top of that definition.
## Setting
**The class $EG$ and its constructible core.** `Chou.ElementaryAmenable G` is an inductive
predicate on groups: finite groups and abelian groups are in the class, and the class is closed
under isomorphism, subgroups, quotients, extensions and directed unions of subgroups; each rule
is a constructor of the published bundle, where it is stated precisely. Chou builds the hierarchy $EG_0 \subseteq EG_1 \subseteq \cdots$
by transfinite recursion, applying only extensions and directed unions to the finite and
abelian groups, and proves that $\bigcup_\alpha EG_\alpha$ is closed under subgroups and
quotients, hence equals $EG$. The union $\bigcup_\alpha EG_\alpha$ is realised here without
ordinals, as the inductive predicate `Chou.Constructible`, whose constructors are `of_finite`,
`of_commGroup`, `of_mulEquiv`, `extension` and `directedUnion`; Chou's transfinite induction
over $\alpha$ becomes structural induction over a derivation, with the same case analysis.
**Periodic and locally finite groups.** A group is periodic if every element has finite order
(Mathlib's `IsMulTorsion`) and locally finite if every finitely generated subgroup is finite
(`Chou.IsLocallyFinite`). Day's class $NF$ is `Chou.NoFreeSubgroupOfRankTwo`: no homomorphism
from the free group on two generators into $G$ is injective.
**Growth.** For a finite generating set $S$ of $G$, `Chou.wordBall S n` is the set of products
of at most $n$ factors, each in $S$ or with inverse in $S$. $G$ *has exponential growth* if for
some finite generating set the ball of radius $n$ has at least $c^n$ elements for some $c > 1$
and all $n$; it is *exponentially bounded* if for some finite generating set and every $c > 1$
the balls are eventually smaller than $c^n$. Chou works with $|F^n|$ for products of exactly
$n$ elements of a finite generating set $F$; for $F$ symmetric and containing the identity the
two agree, and Wolf's observation that the growth type is independent of the generating set is
one of the milestones. "Almost nilpotent" is Mathlib's `Group.IsVirtuallyNilpotent`: a
nilpotent subgroup of finite index. A *free subsemigroup on two generators* means two elements
$a, b$ such that distinct positive words in $a, b$ are distinct in $G$
(`Chou.HasFreeSubsemigroupOfRankTwo`).
**Packings.** A pair of subsets $(S, X)$ is a *packing* of $G$ if $(s, x) \mapsto sx$ is a
bijection $S \times X \to G$ (`Chou.IsPacking`), and $G$ has *property (P)* if every finite
subset lies in a finite $S$ for which some $(S, X)$ is a packing (`Chou.HasPackingProperty`).
$G$ is *residually elementary amenable* if every $x \neq 1$ survives in some elementary amenable
quotient (`Chou.ResiduallyElementaryAmenable`).
## Target
The goal is Chou's description of the class, Proposition 2.2 (b) (p. 397): “$EG$ is the smallest
class of groups which contains all finite groups and all abelian groups and is closed under
processes (III) and (IV).” It is stated as the equivalence `ElementaryAmenable G ↔ Constructible G`.
The milestones follow the paper's order.
*Section 2.* Proposition 2.1 in two halves — the constructible groups are closed under
subgroups and under quotients — which is the whole proof of the goal. Theorem 2.3: periodic
elementary amenable groups are locally finite; and its consequence that $NF \setminus EG$ is
nonempty. Corollary 2.4: finitely generated simple elementary amenable groups are finite.
*Section 3.* Lemma 3.1 (an extension of almost nilpotent by almost nilpotent is almost
nilpotent or of exponential growth), Theorem 3.2 and Rosenblatt's sharpening Theorem 3.2′,
together with the facts Chou uses on the way: a finite-by-nilpotent group is almost nilpotent;
a free subsemigroup forces exponential growth; Wolf's independence of the generating set; and
Milnor's existence of the growth rate, in the form "exponentially bounded means not of
exponential growth".
*Section 4.* Property (P) for finite groups, for $\mathbb Z$, for finitely generated abelian
groups; Lemma 4.1 (directed unions and extensions preserve (P)); Proposition 4.2 (every
elementary amenable group has (P)); Lemma 4.6 (a) and Corollary 4.7 (residually elementary
amenable groups have (P)); and the free groups.
## External theorems as milestones
Chou's Section 3 rests on results the paper cites rather than proves, none of which is in Mathlib.
They are stated here as milestones in their own right, so that the dependence is visible and
each is a well-defined target: the Milnor–Wolf theorem (a finitely generated solvable group
that is exponentially bounded is almost nilpotent); M. Hall's theorem that a finitely generated
group has finitely many subgroups of each finite index; that finitely generated nilpotent
groups are finitely presented and that a group with a finitely presented subgroup of finite
index is finitely presented; Milnor's Lemmas 1–2 in the form Chou states on p. 400 (in a
finitely generated exponentially bounded group, a normal subgroup with finitely presented
quotient is finitely generated); and Rosenblatt's variant of Lemma 3.1. Section 4 needs one
more: free groups are residually finite. Lemma 3.1 and Theorems 3.2, 3.2′ can be closed only
once these are; every other milestone is provable from Mathlib and the published library.
**Two remarks on Theorem 2.3.** Chou's witness for $NF \setminus EG$ is a periodic group that is
not locally finite (Golod; Novikov–Adjan), whose existence is not formalized. The platform
already holds a different witness: Thompson's group $F$ is not elementary amenable
(Cannon–Floyd–Parry, Theorem 4.10) and has no free subgroup on two generators (Brin–Squier);
both are published and proved, and the milestone may be closed by them. The inclusion
$EG \subseteq NF$ itself is von Neumann's theorem that amenable groups contain no free subgroup
of rank two, which passes through the definition of amenability and is not part of this
mission.
## What is left out
The ordinal-indexed hierarchy $EG_\alpha$ and the remark that it stabilises at some
$\alpha_0 + 1$ (Proposition 2.2 (a)) are replaced by the inductive predicate. Chou's two
examples of finitely generated groups in $EG$ that are not almost solvable (p. 402), the
Golod–Shafarevich discussion, and Lemma 4.6 (b) (ordinal-indexed normal series) are omitted.
Propositions 4.3–4.5 on almost convergent sets, and Milnor's remark that exponentially bounded
groups are amenable, need invariant means on $\ell^\infty(G)$ and belong to a mission on
amenability itself.
## References
- C. Chou, *Elementary amenable groups*, Illinois J. Math. 24 (1980), 396–407.
- M. M. Day, *Amenable semigroups*, Illinois J. Math. 1 (1957), 509–544.
- J. Milnor, *Growth of finitely generated solvable groups*, J. Differential Geometry 2 (1968),
447–449; J. A. Wolf, *Growth of finitely generated solvable groups and curvature of Riemannian
manifolds*, ibid. 421–446.
- J. M. Rosenblatt, *Invariant measures and growth conditions*, Trans. Amer. Math. Soc. 193
(1974), 33–53.
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Math. 42 (1996), 215–256 (Theorem 4.10); M. G. Brin, C. C. Squier, *Groups of
piecewise linear homeomorphisms of the real line*, Invent. Math. 79 (1985), 485–498.
56 thms2 active usersReviewed
🏆Completed
Captain: dbenbenn
Cannon–Floyd–Parry: the two presentations of Thompson's group FTextbook
## Motivation
Thompson's group $F$ is the group of piecewise-linear order-preserving homeomorphisms of
$[0,1]$ with finitely many breakpoints, all at dyadic rationals, and all slopes powers of $2$.
Two earlier missions formalize its definition and its first structural facts
([§1 and §4](https://prove2.me/missions/Cannon%E2%80%93Floyd%E2%80%93Parry%3A%20Thompson%27s%20group%20F%20and%20the%20simplicity%20of%20its%20commutator%20subgroup):
the commutator subgroup is simple, $F$ is not elementary amenable) and its tree-diagram normal
form ([§2](https://prove2.me/missions/Cannon-Floyd-Parry%3A%20tree%20diagrams%20and%20the%20normal%20form%20for%20Thompson%27s%20group%20F)).
What neither says is how $F$ looks *as an abstract group*: by generators and relations.
That is §3 of Cannon, Floyd and Parry's *Introductory notes on Richard Thompson's groups*
(L'Enseignement Math. 42 (1996), [doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877)),
which gives two presentations of $F$ and proves that both present the group of
homeomorphisms:
$$F_1 = \langle A, B \;:\; [AB^{-1}, A^{-1}BA],\ [AB^{-1}, A^{-2}BA^{2}] \rangle,
\qquad
F_2 = \langle X_0, X_1, X_2, \dots \;:\; X_k^{-1} X_n X_k = X_{n+1} \text{ for } k < n \rangle .$$
The finite presentation is the form in which $F$ enters most of the literature — the word
problem, the growth and amenability questions, the homological results of Brown and
Geoghegan all start from it — and the infinite presentation is the one that makes the
normal form of §2 visible as an algebraic fact.
## Setting
Throughout, $[x, y] = x y x^{-1} y^{-1}$, the source's convention, and groups are written
multiplicatively with composition of maps as the product: $(f g)(t) = f(g(t))$.
**The functions.** $A$ and $B$ are the two specific homeomorphisms of $[0,1]$ from the §1
mission (`mapA`, `mapB`: $A$ halves $[0, \tfrac12]$, is a translation on $[\tfrac12,\tfrac34]$,
and doubles $[\tfrac34, 1]$; $B$ is the identity on $[0,\tfrac12]$ and acts like $A$, scaled,
on $[\tfrac12, 1]$). For $n \ge 1$, $X_n = A^{-(n-1)} B A^{n-1}$ and $X_0 = A$; these are the
functions `X n` of the §2 bundle. Corollary 2.6 of the source, proved in the §2 mission, says
$A$ and $B$ generate $F$.
**The formal symbols.** $F_1$ and $F_2$ are *presented groups*: the free group on the listed
symbols modulo the normal closure of the listed relators. In Lean they are Mathlib's
`PresentedGroup` applied to explicit relator sets: `relsF1`, a two-element set of words in
the free group on the two-element type `FormalAB`, and `relsF2`, the set of words
$X_k^{-1} X_n X_k X_{n+1}^{-1}$ for $k < n$ in the free group on $\mathbb{N}$. The symbols
are distinct objects from the functions; the whole content of the section is that the map
"symbol $\mapsto$ function" is an isomorphism.
**Auxiliary objects.** In $F_1$ the source sets $Y_0 = A$ and $Y_n = A^{-(n-1)} B A^{n-1}$
for $n \ge 1$ (`Y`), the intended images of the $X_n$. In $F_2$ a list of nonnegative
exponents $c_0, \dots, c_n$ determines the positive word $X_0^{c_0} X_1^{c_1} \cdots X_n^{c_n}$
(`wordF2`), the formal counterpart of the §2 bundle's `word`; the normal-form conditions of
Corollary-Definition 2.7 are the §2 predicate `IsNormalFormData`, reused verbatim.
## Target
The goal is the finite presentation, Theorem 3.4 for $F_1$:
$$\text{there is a group isomorphism } F_1 \xrightarrow{\ \sim\ } F \text{ with } A \mapsto A,\ B \mapsto B .$$
On the way, in the order the source proves them:
$$F_1 \cong F_2 \text{ with } A \mapsto X_0,\ B \mapsto X_1 \quad\text{(Theorem 3.1)},
\qquad
F_2 \cong F \text{ with } X_n \mapsto X_n \quad\text{(Theorem 3.4 for } F_2) .$$
A one-line consequence closes the list: $F$ is finitely presented, in Mathlib's sense
`Group.IsFinitelyPresented`.
## Significance
*The result.* A presentation is what makes $F$ an object of combinatorial group theory. The
two relators are what one checks a homomorphism against, the infinite presentation is what
the normal form is a normal form *for*, and "finitely presented" is the hypothesis under
which $F$ is a test case for conjectures about finitely presented groups. Every later
algebraic statement about $F$ — the word problem is solvable, the abelianization is
$\mathbb{Z}^2$, the automorphism group, the presentations of $T$ and $V$ — is stated relative
to one of these two presentations.
*Formalizing it.* Both theorems are proved in the source and their proofs are short, so what
this mission produces is the machine-checked bridge between the two existing developments:
the analytic definition of $F$ and its tree-diagram normal form on one side, an abstract
presented group on the other. The isomorphism $F_2 \cong F$ is where §2's uniqueness theorem
is *used* rather than merely proved: injectivity of $F_2 \to F$ is exactly the statement that
distinct normal forms give distinct functions. Nothing here is machine-checked anywhere else;
the platform has no presentation of $F$.
## Difficulty
Theorem 3.1 is a computation in $F_1$ and offers no surprises once lines (3.2) and (3.3) of
the source are set up as their own statements: the induction that establishes
$Y_k^{-1} Y_n Y_k = Y_{n+1}$ from the two relators is the only place care is needed, and the
source spells it out.
The central difficulty is the paragraph on p. 226 proving that $F_2 \to F$ is injective. The
source argues in prose that "every nontrivial element $x$ of $F_2$ can be expressed as a
positive element times a negative element", and then "put in normal form" by deleting an
$X_k$ from both parts and re-indexing when $X_{k+1}$ is absent. Formally this is a rewriting
argument inside the abstract group $F_2$, with no geometry to lean on: one needs the three
derived relations $X_k^{-1} X_n = X_{n+1} X_k^{-1}$, $X_n^{-1} X_k = X_k X_{n+1}^{-1}$,
$X_n X_k = X_k X_{n+1}$ (for $k < n$), an induction that sorts an arbitrary word into
positive-times-negative form, and a second induction that reduces such a form until the
normal-form conditions hold. The obvious shortcut — "every element of $F_2$ is the image of
some function, and functions have normal forms" — is circular, because it presupposes the
injectivity being proved. The milestone `exists_isNormalFormData_F2` isolates this step.
## Formalization scope
- $F$, $A$, $B$, the functions $X_n$, the words `word`/`wordFrom` and the predicate
`IsNormalFormData` are the published definitions of the §1 and §2 missions
(`CannonFloydParry`, `CannonFloydParry_Trees`, `CannonFloydParry_TreeDiagrams`), imported
unchanged. Elements of $F$ are order isomorphisms of the subtype $[0,1] \subset \mathbb{R}$,
and $F$ is the subgroup they generate; membership of $A$, $B$, $X_n$ in $F$ is a proved
theorem, not a definition.
- The new bundle `CannonFloydParry_Presentations` adds only the formal side: the symbol type
`FormalAB`, the relator sets `relsF1`, `relsF2`, the presented groups `F1`, `F2`, the
symbol maps `symF2` (into $F_2$) and `symF` (into the interval maps), the elements `Y`, and
the words `wordF2`. Relators are written out as $x y x^{-1} y^{-1}$; no commutator notation
is used in published statements.
- Isomorphisms are stated as existence of a `MulEquiv` sending the named generators to the
named images. Nothing is asserted about uniqueness of the isomorphism (it is unique, since
the generators generate).
- A trivializing reading is ruled out by the generator conditions: an isomorphism between
$F_1$ and $F$ that ignored the symbols would be meaningless, so every statement pins the
images of $A$ and $B$ (or of every $X_n$).
- Reused platform theorems: Corollary 2.6 (`closure_mapA_mapB_eq_F`), the §2 normal-form
theorems (`exists_isNormalFormData`, `word_ne_one_of_isNormalFormData`), and the §4
mission's `mem_commutator_iff` if a solver prefers to verify the relators of $F_1$ in $F$
through supports rather than by direct computation. Solutions may import them.
- Welcome contributions beyond the milestone list: a Lean statement of the *presentation
with two generators and two relators* as a `Group.IsFinitelyPresented` instance built from
the isomorphism (the last milestone), and, further off, the presentations of $T$ and $V$
from §5–§6, which extend $F_1$ by one and two generators.
## Selected references
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Mathématique (2) 42 (1996) 215–256, §3 pp. 225–226.
[doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877)
- K. S. Brown, R. Geoghegan, *An infinite-dimensional torsion-free $FP_\infty$ group*,
Inventiones Math. 77 (1984) 367–381. [doi:10.1007/BF01388451](https://doi.org/10.1007/BF01388451)
- M. G. Brin, C. C. Squier, *Groups of piecewise linear homeomorphisms of the real line*,
Inventiones Math. 79 (1985) 485–498. [doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519)
21 thms1 active userReviewed
🏆Completed
Captain: dbenbenn
Cannon-Floyd-Parry: tree diagrams and the normal form for Thompson's group FTextbook
## Why tree diagrams
**Thompson's group $F$** is a finitely presented group of piecewise-linear homeomorphisms of the
unit interval that has served since the 1960s as a standard supply of counterexamples in
combinatorial group theory: its commutator subgroup is simple, every proper quotient of it is
abelian, it contains no free subgroup of rank two, it is not elementary amenable, and whether it
is amenable is a question Cannon, Floyd and Parry report as having been raised by Geoghegan in
1979 and still open when they wrote
([CFP96](https://doi.org/10.5169/seals-87877), §4 and p. 227).
Almost nothing about $F$ is computed directly from that analytic definition. What makes the group
tractable is a combinatorial calculus: each element is encoded by a pair of finite binary trees,
and multiplication becomes a cancellation between trees. Cannon, Floyd and Parry credit the
device to Brown and devote §2 of their notes to it; everything later in those notes that requires
a computation — the two presentations of §3, the normal subgroup lattice of §4, the treatment of
Thompson's group $T$ in §5 — runs through it.
This mission formalizes that calculus and the normal form it yields.
## Setting
A real number is **dyadic** when it has the form $m/2^k$ with $m$ an integer and $k$ a
nonnegative integer. **Thompson's group $F$** consists of the increasing homeomorphisms of
$[0,1]$ that are piecewise linear with finitely many breakpoints, all breakpoints dyadic and
every slope an integer power of $2$, under composition. Two of its elements are
$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\
2x-1 & \tfrac34 \le x \le 1\end{cases} \qquad
B(x) = \begin{cases} x & 0 \le x \le \tfrac12\\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34\\
x - \tfrac18 & \tfrac34 \le x \le \tfrac78\\ 2x-1 & \tfrac78 \le x \le 1,\end{cases}$$
and from them come $X_0 = A$ and $X_n = A^{-(n-1)} B A^{n-1}$ for $n \ge 1$, so that
$X_1 = B$.
A **standard dyadic interval** is one of the form $[a/2^n, (a+1)/2^n]$ with $a$ and $n$
nonnegative integers and $a+1 \le 2^n$. A partition $0 = x_0 < \cdots < x_m = 1$ of $[0,1]$ is a
**standard dyadic partition** when every $[x_{i-1}, x_i]$ is a standard dyadic interval.
An **ordered rooted binary tree** is a finite tree in which each vertex has either no children or
an ordered left child and right child. Its childless vertices are its **leaves**, which carry a
canonical left-to-right order; its **right side** is the path from the root always taking the
right child; a **caret** is a vertex with its two children. Assigning $[0,1]$ to the root and
splitting each interval at its midpoint between the two children gives every vertex a standard
dyadic interval, and the leaves then cut out a standard dyadic partition — the sense in which
such a tree is a **$\mathcal{T}$-tree**. The **exponents** of a $\mathcal{T}$-tree are one
nonnegative integer per leaf, in order: the $k$th is the length of the longest arc of left edges
beginning at the $k$th leaf that does not reach the right side.
A **tree diagram** is an ordered pair $(R,S)$ of $\mathcal{T}$-trees with equally many leaves. An
element $f$ of $F$ **has** that diagram when $f$ is affine on each interval cut out by the leaves
of $R$ and carries those intervals, in order, onto the intervals cut out by the leaves of $S$.
Adjoining a caret to $R$ and to $S$ at the same leaf gives another diagram for the same $f$; a
diagram admitting no such reduction — no position where both trees carry a caret — is
**reduced**.
## Formalization targets
### Goal: the unique normal form
Every $f \ne 1$ in $F$ is
$$f \;=\; X_0^{b_0} X_1^{b_1} \cdots X_n^{b_n} \, X_n^{-a_n} \cdots X_1^{-a_1} X_0^{-a_0}$$
for exactly one choice of nonnegative integers $n$, $a_0, \dots, a_n$, $b_0, \dots, b_n$ subject
to two conditions: exactly one of $a_n$ and $b_n$ is nonzero, and if $a_k > 0$ and $b_k > 0$ for
some $k < n$ then $a_{k+1} > 0$ or $b_{k+1} > 0$.
It fixes no bound on $n$ and no normalization beyond those two conditions, so no later
refinement of how the exponents are presented can invalidate it.
### Along the way
The milestone list follows §2 in order: the correspondence between standard dyadic partitions
and $\mathcal{T}$-trees, the bijection between $F$ and the reduced tree diagrams, the word read
off the exponents of $(R,S)$, a criterion for a diagram to be reduced, generation by $A$ and
$B$, and closure under multiplication of the **positive** elements — those of the form
$X_0^{b_0} \cdots X_n^{b_n}$ with every exponent nonnegative.
## What it gives
A normal form is a decision procedure: two words in the generators name the same element exactly
when their normal forms agree, so the word problem for $F$ is solved by computing them. The
generation statement is what licenses treating $F$ as a two-generator group, and it is the input
to both presentations in §3. The positive elements and their closure under multiplication are
used, with the normal form, throughout §5 on Thompson's group $T$.
The §2 results this mission targets — Lemma 2.2, the correspondence between $F$ and the
reduced tree diagrams, Theorem 2.5, Corollary 2.6, Corollary-Definition 2.7 and Lemma 2.8 — are
**proved** mathematics: Cannon, Floyd and Parry are expounding material that goes back to
Thompson's unpublished notes. None of them has a machine-checked proof on this platform, and the
library contains no tree-diagram machinery to build on, so the definitions published here fix the
interface for anyone later formalizing Thompson's groups $T$ and $V$, which occupy the same notes
and are built from the same trees.
There is also a concrete dependency. The companion mission on §4 of the same paper has eleven of
its fifteen milestones machine-checked, and **all four that remain wait on this section**: Cannon,
Floyd and Parry prove their Theorem 4.1 through Corollary 2.6 and their Theorem 4.3 through the
normal form. Corollary 2.6 appears in this milestone list as the same theorem object that is open
there, so closing it here closes it there.
## Difficulty
The obvious way to attach a diagram to an element $f$ is to use the partition given by its
breakpoints. That fails twice over: the breakpoints of $f$ need not be the division points of any
$\mathcal{T}$-tree, and even when they are, their images under $f$ need not be either, since the
definition of $F$ constrains the breakpoints and slopes of $f$ and says nothing about where the
image partition sits. Both failures must be repaired by refining the partition before any tree
appears, which is why that refinement is a milestone rather than a preliminary.
Uniqueness of the reduced diagram is a difficulty of a different kind: two reduced diagrams for
the same element admit no a priori map between their trees, so they cannot be compared directly.
A third is not visible in the source. For trees with $n+1$ leaves the exponent lists always end
in $0$, so the outermost factors of the word above vanish; but the normal form demands that
exactly one of $a_n$, $b_n$ be nonzero. The two indexings differ, and a re-indexing step sits
between the theorem producing the word and the corollary stating the normal form. The paper prints
them one under the other. That step is a milestone of its own, flagged as absent from the source,
so a solver working from the paper alone is not ambushed by it.
## Formalization scope
Ordered rooted binary trees are an inductive type — a leaf, or a pair of subtrees — rather than
graphs with a root and valence conditions. Those conditions say exactly that every non-leaf vertex
has two distinguished children, so both descriptions pick out the same objects, but the inductive
type is a **reformulation** of the paper's definition and the definition bundle says so. The
infinite tree of all standard dyadic intervals is likewise never built: the subdivision of
$[0,1]$ comes from a recursion halving at each node, which turns the paper's observation that the
leaves of a $\mathcal{T}$-tree are the intervals of a standard dyadic partition from something
given into something proved.
$F$ is imported rather than redefined, from the published definition bundle of the companion
mission, where it is the subgroup generated by the piecewise-linear maps described above;
membership in that subgroup is identified with the piecewise-linear description by a theorem
already machine-checked there. Exponent data is carried by finite lists, and the uniqueness in
the goal is uniqueness of that list data.
The goal is vacuous in neither direction: its hypothesis is met by $A$ and $B$ themselves, and a
separate milestone asserts that every choice of exponent data meeting the two conditions names an
element other than the identity.
The tree combinatorics — leaf counts, right sides, the subdivision map, the exponents,
carets — is published here as a separate definition node that mentions $F$ nowhere and needs
nothing but Mathlib, so it is reusable as it stands; the diagram vocabulary is built on it. Any
milestone is open to contribution, as are routes other than the paper's.
## Selected references
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Mathématique (2) **42** (1996), 215–256.
[doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877) — §2, pages 218–224, is the
source for this mission; §1, page 217, defines $A$, $B$ and the $X_n$.
Within that paper tree diagrams are credited to Brown and the word-length algorithm to Fordham,
cited there as [Bro1] and [Fo].
19 thms2 active usersReviewed
🏆Completed
Captain: dbenbenn
Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroupTextbook
## Motivation
This mission formalizes §4 of Cannon, Floyd and Parry's *Introductory notes on Richard
Thompson's groups*, together with the definition of **Thompson's group $F$** from their §1.
The goal is their Theorem 4.5: the commutator subgroup $[F,F]$ is simple.
In the 1960s Richard Thompson defined three groups, now written $F$, $T$ and $V$, whose
properties have kept them in use ever since as a source of examples at the edge of what
groups can do. $F$ is the smallest of the three and the least understood. It is finitely
presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and
whether it is **amenable** — whether it carries a finitely additive left-invariant probability
measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that
Geoghegan raised the question and conjectured in 1979 both that $F$ contains no non-Abelian
free subgroup and that $F$ is not amenable.
That question is what makes $F$ worth pinning down precisely. Write $AG$ for the class of
amenable discrete groups, $EG$ for the elementary amenable ones, and $NF$ for the groups with
no free subgroup of rank two. That $AG \subset NF$ was noted by
[Day](https://doi.org/10.1215/ijm/1255380675) and follows from
[von Neumann](https://doi.org/10.4064/fm-13-1-73-116); whether it is strict is the **von
Neumann–Day problem**. It is: Olshanskii proved $AG \neq NF$ in a 1984 ICM address and
[Gromov](https://doi.org/10.1007/978-1-4613-9586-7_3) gave an independent proof — but by
examples that are not finitely presented. Brin and Squier proved in 1985 that $F \in NF$, and
$F$ is known not to be elementary amenable (Theorem 4.10 of the source, out of scope here). So
$F$ is a finitely presented group in $AG \setminus EG$ if it is amenable and in
$NF \setminus AG$ if it is not — a question with no other finitely presented candidate.
## Setting
Call a real number **dyadic** if it has the form $m/2^{k}$ with $m \in \mathbb{Z}$ and
$k \in \mathbb{N}$.
**Thompson's group $F$**, as §1 of the source defines it, is the set of piecewise linear
homeomorphisms of the closed unit interval $[0,1]$ onto itself that are differentiable except
at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of $2$.
Since those derivatives are positive, every element preserves orientation, so the elements of
$F$ are increasing. Composition of two such maps is again one, and so is the inverse of one,
so $F$ is a group.
The formalization calls such a map **piecewise linear over the dyadics**, and defines $F$ as
the subgroup *generated by* those maps — so that closure under composition and inverses is a
theorem rather than part of the construction, as the source has it. What the model fixes rather
than derives is under **Formalization scope** below.
Two particular elements generate it. Write
$$A(x) = \begin{cases} x/2 & 0 \le x \le \tfrac12\\ x - \tfrac14 & \tfrac12 \le x \le \tfrac34\\ 2x-1 & \tfrac34 \le x \le 1\end{cases}
\qquad
B(x) = \begin{cases} x & 0 \le x \le \tfrac12 \\ x/2 + \tfrac14 & \tfrac12 \le x \le \tfrac34 \\ x - \tfrac18 & \tfrac34 \le x \le \tfrac78 \\ 2x-1 & \tfrac78 \le x \le 1.\end{cases}$$
An element of $F$ is **trivial near $0$** if it fixes every point of some interval
$[0,\varepsilon)$, and **trivial near $1$** if it fixes every point of some
$(1-\varepsilon, 1]$. The **support** of $f$ is the set of points of $[0,1]$ that $f$ moves.
The commutator convention throughout is $[x,y] = xyx^{-1}y^{-1}$, and $[F,F]$ denotes the
commutator subgroup.
## Formalization targets
### Goal
$$[F,F] \ \text{is a simple group.}$$
This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than
itself and the trivial one. It is the goal because the rest of the section feeds it — both
halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its
proof.
### Theorem 4.1, which has two parts
$$[F,F] \;=\; \{\, f \in F : f \text{ is trivial near } 0 \text{ and near } 1 \,\}$$
$$F/[F,F] \;\cong\; \mathbb{Z} \oplus \mathbb{Z}$$
### Theorem 4.3
$$N \trianglelefteq F,\ N \neq 1 \;\Longrightarrow\; F/N \text{ is Abelian}$$
So $F$ has no interesting proper quotients at all. With the first part of Theorem 4.1 this
forces every nontrivial normal subgroup of $F$ to contain $[F,F]$.
### Supporting results
That the piecewise-linear maps are already closed under composition and inverses, so that $F$
consists of exactly those maps; a transitivity lemma on dyadic partitions of $[0,1]$; the fact
that the subgroup of elements supported in a dyadic interval $[a,b]$ of dyadic length is
isomorphic to $F$ itself; triviality of the center; that $F$ contains no non-Abelian free group;
and that $F$ admits a total order invariant under multiplication on both sides.
## Significance
**What the results give.** Theorem 4.1 identifies $[F,F]$ concretely — a subgroup defined by a
global algebraic condition turns out to be cut out by local behavior at the two endpoints —
and computes the abelianization, making the pair of endpoint slopes a complete invariant of $F$
modulo commutators. Theorem 4.3 and the simplicity of $[F,F]$ together determine the whole
normal subgroup lattice: every normal subgroup of $F$ is trivial or contains $[F,F]$. That
lattice is the input to the elementary-amenability argument.
**What formalizing adds.** All of these are proved in the source; none is in Mathlib, which
has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are
proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements
of $F$ permute the dyadic rationals, that $F$ embeds in the group Brin and Squier work with, and
the absence of a free subgroup of rank two, which follows from the already-formalized
Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness,
dyadic-breakpoint bookkeeping, extension by the identity — is reusable for $T$, for $V$, and
for the wider family of piecewise-linear homeomorphism groups.
## Difficulty
The obvious approach to the goal is to argue that a normal subgroup of $[F,F]$ containing a
nontrivial element must be everything, by conjugating that element around. It fails on its own:
an element of $[F,F]$ is pinned down only by being trivial near the two endpoints, and one still
has to manufacture — inside $[F,F]$, not merely inside $F$ — an element carrying a prescribed
pair of neighborhoods into those. That construction is what the dyadic-partition transitivity
lemma supplies, and it is where the combinatorics of dyadic subdivision enters.
The second difficulty was that the source proves §4 using the tree-diagram normal form of §2.
That section is now formalized in its own mission, *Cannon–Floyd–Parry §2: tree diagrams and the
normal form* (mission `ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8`), all of whose milestones are proved.
Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem
2.5 (`represents_word_exponents`) and the normal form (`existsUnique_normalForm`) are available to
a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file
imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions
are public and written to be reused that way. The piecewise-linear route — dyadic-partition
transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own
argument uses.
## Formalization scope
The unit interval is $[0,1] \subseteq \mathbb{R}$ as a subtype, and an element of $F$ is an
order isomorphism of it, so orientation preservation is built into the representation rather
than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise
linearity is stated as: there is a finite set $B$ of dyadic reals such that the map is affine,
with slope a power of two, on every closed interval whose interior misses $B$. Intercepts are
**not** required to be dyadic — that is derived by induction along the breakpoints, not part of
the definition.
The definition is not vacuous: $A$ and $B$ of Example 1.1 are constructed explicitly, and that
$F$ is not the trivial group is one of the milestones below — so no statement here is satisfied
by the trivial group. In particular the goal, which asserts simplicity and therefore
nontriviality, is not trivially false.
A companion definition places the same data on the real line, each element extended by the
identity outside $[0,1]$; that line realisation is what the bridge statement connects to Brin
and Squier's group. Corollaries 4.6, 4.7 and 4.10 of the source are out of scope: they need free
products of monoids, growth of finitely generated groups, and the transfinite class of
elementary amenable groups respectively, none of which Mathlib has.
## Selected references
- J. W. Cannon, W. J. Floyd, W. R. Parry, *Introductory notes on Richard Thompson's groups*,
L'Enseignement Mathématique (2) **42** (1996), 215–256.
[doi:10.5169/seals-87877](https://doi.org/10.5169/seals-87877)
- M. G. Brin, C. C. Squier, *Groups of piecewise linear homeomorphisms of the real line*,
Inventiones Mathematicae **79** (1985), 485–498.
[doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519)
- C. Chou, *Elementary amenable groups*, Illinois Journal of Mathematics **24** (1980), 396–407.
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)
- M. M. Day, *Amenable semigroups*, Illinois Journal of Mathematics **1** (1957), 509–544.
[doi:10.1215/ijm/1255380675](https://doi.org/10.1215/ijm/1255380675)
- J. von Neumann, *Zur allgemeinen Theorie des Maßes*, Fundamenta Mathematicae **13** (1929),
73–116. [doi:10.4064/fm-13-1-73-116](https://doi.org/10.4064/fm-13-1-73-116)
- A. Yu. Olshanskii, *On a geometric method in the combinatorial group theory*, Proceedings of
the International Congress of Mathematicians (Warsaw, 1983), vol. 1, 1984, pp. 415–424.
[IMU archive](https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1983.1/ICM1983.1.ocr.pdf)
- M. Gromov, *Hyperbolic groups*, in *Essays in Group Theory* (S. M. Gersten, ed.), MSRI
Publications **8**, Springer, 1987, pp. 75–263.
[doi:10.1007/978-1-4613-9586-7_3](https://doi.org/10.1007/978-1-4613-9586-7_3)
34 thms3 active usersReviewed
🏆Completed
Captain: burkh4rt
Herzog-Schönheim for subnormal coversResearch Paper
## Motivation
A **coset partition** of a group $G$ is a finite family of left cosets $a_1G_1, \dots, a_kG_k$
that are pairwise disjoint and cover $G$. In 1974 [Herzog and
Schönheim](https://doi.org/10.4153/CMB-1974-025-7) asked whether the indices
$n_i = [G : G_i]$ of such a partition, with $k > 1$, can be pairwise distinct. They cannot when
$G = \mathbb{Z}$ — there a coset partition is an *exact covering system* of the integers, and
Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups
the question is still open, even for finite solvable groups.
Progress has come in two styles. *Structural*: Berger, Felzenbaum and Fraenkel settled finite
**nilpotent** groups in [Canad. Math. Bull. 29 (1986)
329–333](https://doi.org/10.4153/CMB-1986-050-0) and finite **pyramidal** groups in [Fund. Math.
128 (1987) 139–144](https://doi.org/10.4064/fm-128-3-139-144). *Order-bounded*: [Ginosar and
Schnabel (2011)](https://www.researchgate.net/publication/265126234) settled every $G$ whose
order has at most two prime divisors, and [Margolis and Schnabel
(2019)](https://arxiv.org/abs/1803.03569) verified all $|G| < 1440$.
The paper formalized here, [Z.-W. Sun, *J. Algebra* **273** (2004)
153–175](https://doi.org/10.1016/S0021-8693(03)00526-X), takes a third route: it constrains the
*subgroups* rather than the group, and simultaneously weakens "partition" to "uniform cover".
Its hypothesis — that the $G_i$ be **subnormal** — costs nothing in the nilpotent case (every
subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient
groups $G$. It also answers negatively an open question of the same paper, generalizing one of
Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.
## Setting
Let $G$ be a group, written multiplicatively. For a finite system
$$ \mathcal{A} = \{a_iG_i\}_{i=1}^{k} $$
of left cosets, the **covering function** counts memberships,
$$ w_{\mathcal{A}}(x) \;=\; \bigl|\{\, 1 \le i \le k \;:\; x \in a_iG_i \,\}\bigr| . $$
If $w_{\mathcal{A}}$ is constant, say $w_{\mathcal{A}} \equiv w$, then $\mathcal{A}$ is a
**uniform cover** of $G$ of weight $w$; the case $w = 1$ is exactly a coset partition. A uniform
cover is **trivial** when $G_i = G$ for every $i$, and this is the only degenerate case that must
be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint
subcover at all.
A subgroup $H \le G$ is **subnormal** if some finite chain
$H = H_0 \trianglelefteq H_1 \trianglelefteq \cdots \trianglelefteq H_n = G$ reaches $G$, each
term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is;
and $\operatorname{Sym}(4)$ shows a subgroup of a solvable group need not be.
Write $n_i = [G : G_i]$ for the indices, always assumed finite, and
$$ N \;=\; [\,n_1, \dots, n_k\,] $$
for their least common multiple, whose prime divisors are exactly those of $n_1\cdots n_k$. Let
$p_*$ and $p^*$ denote the least and greatest prime divisors of $N$, let $\varphi$ be Euler's
totient, and let
$$ M \;=\; \max_{1 \le j \le k} \bigl|\{\, 1 \le i \le k : n_i = n_j \,\}\bigr| $$
be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says
$M \ge 2$.
## Target
The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by
cosets of subnormal subgroups of finite index, some index divisible by the largest prime $p^*$ is
repeated at least $p_*$ times,
$$ \exists\, j, \qquad p^* \mid n_j \quad\text{and}\quad
\bigl|\{\, i : n_i = n_j \,\}\bigr| \;\ge\; p_* . $$
In particular $M \ge p_*$. Two weaker consequences are separate targets. Since $p_* \ge 2$, this
gives the **Herzog–Schönheim conjecture for subnormal uniform covers**,
$$ \exists\, i \ne j, \qquad [G : G_i] = [G : G_j], $$
and the quantitative step behind it is a **Burshtein-type inequality**, which after clearing
denominators reads
$$ p^{*}\prod_{p \mid N}(p-1) \;<\; \bigl|\{\, i : n_i = n_j \,\}\bigr| \prod_{p \mid N} p
\qquad\text{for some } j \text{ with } p^* \mid n_j . $$
## Significance
*The result itself.* It is the widest structural class in which Herzog–Schönheim is known, and
the only one that does not require $G$ to be finite: subnormality of the $G_i$ is a condition on
the *subgroups*, so $G$ itself is arbitrary. It strictly contains the nilpotent case of
Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in
this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower
bound on $M$ growing with $p_*$, it answers the paper's open question: one cannot make all the
indices of a uniform cover large while keeping every multiplicity bounded.
*Formalizing it.* Nothing here is open, and the mission is the machine-checked version of a known
proof. What it adds is a formal vocabulary for *uniform* covers — Mathlib has
`Mathlib/GroupTheory/CosetCover.lean` (B. H. Neumann's theorems, $\sum_i 1/[G:H_i] \ge 1$) but no
notion of covering multiplicity — and the arithmetic of subnormality, in particular that
$[G : \bigcap_i G_i]$ *divides* $\prod_i [G : G_i]$ when the $G_i$ are subnormal. Mathlib has
`Subgroup.IsSubnormal` with the basic closure properties but nothing about indices of subnormal
subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure
this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation
(14), already proved on the platform as `BFFPyramidal.muMeasure_divisorClosure_image_mul`, and
this mission reuses that definition file rather than duplicating it.
**Status disclosure.** Complete Lean proofs of the goal and of every milestone below already
exist and will be submitted at launch, so this mission is not an open frontier: its value is the
verified artifact, the reusable vocabulary, and the fact that the development turned up two
places where the published argument needs repair or can be simplified (see *Formalization
scope*). Alternative proofs, sharper variants, and the analytic parts excluded below remain
genuinely open contributions.
## Difficulty
The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform
cover of weight $w$ satisfies $\sum_i 1/n_i = w$, and pairwise distinct $n_i$ can do that.
The real obstruction is that **a cover does not descend to a quotient**. A part $a_iG_i$ need not
lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent
case has nothing to induct along once $G$ may be infinite and the $G_i$ are merely subnormal.
Sun's replacement is a lower bound for the *size of a union of cosets*, Theorem 3.1: if
$H \le G_i$ for all $i$ and $[G:H] < \infty$, then the number of cosets of $H$ inside
$\bigcup_i a_iG_i$ is at least the number of $n < [G:H]$ divisible by some $n_i$. The union is
compared not with the $G_i$ but with a purely numerical shadow of itself in
$\{0, 1, \dots, [G:H]-1\}$, and it is here that subnormality enters, through the divisibility
$[G : \bigcap G_i] \mid \prod [G : G_i]$ (Lemma 2.1) — for arbitrary finite-index subgroups
Poincaré gives only the inequality $[G : \bigcap G_i] \le \prod [G:G_i]$, which is too weak.
The second difficulty is arithmetic and is where the source spends its effort. Turning
Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a
union $\bigcup_i n_i\mathbb{Z}$, and the identity the paper uses (Lemma 3.4) expresses that
density as $\prod_{p \in P}\frac{p-1}{p}$ times an **infinite** sum of reciprocals over
$P$-smooth elements of the union. Along that route the full series is needed: truncating it loses
precisely the geometric factors $\bigl(1 - p^{-(1+\delta_p)}\bigr)^{-1}$ that produce the divisor
sum $\sum_{d \mid N/g} 1/d$ in the conclusion.
It is worth saying, though, that this analytic detour is **avoidable** — a solver need not take
it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by
injecting each index $s$ into the divisor $\operatorname{lcm}\{s' : s' \mid x\}/s$, which is
sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately
interesting milestone of the paper, but it is not on the critical path to the goal. The naive
version of the finite estimate — bounding the density below by $1/\min_i n_i$ — is genuinely
false, as $\{4,6,9,12,18,36\}$ shows, so the injection is the content, not a one-liner.
## Formalization scope
The development commits to the following conventions, worth stating because the prose leaves them
implicit.
Covers are indexed families rather than sets of cosets: `IsUniformCover K a w` asserts that for
every $x$ the number of indices $i$ with $(a_i)^{-1}x \in K_i$ is exactly `w`, counted as
`Nat.card` of a subtype so that no decidability hypothesis is needed. Indexing by `Fin k` keeps
multiplicities visible, which matters because every conclusion counts indices, not distinct
subgroups. Nontriviality is *never* folded into the definition; it appears as the explicit
hypothesis `∃ i, K i ≠ ⊤`, and without it every statement here is false (take $k=1$, $G_1 = G$).
$G$ is an arbitrary group — **not** assumed finite. Finiteness enters only through
`Subgroup.FiniteIndex` on each $K_i$, which the source assumes implicitly when it writes "the
(finite) indices". Indices are `Subgroup.index` and $[G_i : H]$ is `H.relIndex (K i)`. For a
subgroup $H$ that is *not* assumed normal, `G ⧸ H` is still the type of left cosets and
`Nat.card (G ⧸ H) = H.index`; Theorem 3.1 is stated with that type, since the $H$ it is applied
to is not normal.
Densities are never limits. The density of a union $\bigcup_i n_i\mathbb{Z}$ is taken as the
finite ratio $|\{x < N : \exists i,\ n_i \mid x\}| / N$ for an explicit common multiple $N$,
which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the
left-hand side; the right-hand side genuinely is an infinite sum and is stated with `HasSum` over
$\mathbb{R}$.
Inequalities are cleared of denominators and stated in $\mathbb{N}$ wherever possible, so that
$\sum_{d \mid m} 1/d \le c$ appears as $\sum_{d \in m.divisors} d \le c \cdot m$. Readers should
check the direction: $\mathbb{N}$ subtraction truncates, so $\prod_{p \mid N}(p-1)$ is only the
intended quantity because every $p$ here is prime, hence $\ge 2$.
⚠️ **Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope.** Those bound the primes
dividing the indices, their number, and $\log n_1$ by $e^{\gamma}M\log^2 M + O(M \log M \log\log
M)$ and similar, and they rest on **Mertens' third theorem**,
$\prod_{p \le x}(1 - 1/p) \sim e^{-\gamma}/\log x$, which Mathlib does not have. It is worth
being precise about what Mathlib *does* have, since the gap is narrower than it looks: the prime
counting function `Nat.primeCounting`, Chebyshev's $\theta$ and $\psi$ with the machinery around
them (`Mathlib/NumberTheory/Chebyshev.lean`), Euler products
(`Mathlib/NumberTheory/EulerProduct/`), and the constant $\gamma$ itself
(`Real.eulerMascheroniConstant`) are all present — what is missing is Mertens' asymptotic tying
them together, and the $\pi(x)$ asymptotics. Supplying that is a substantial number-theory
project in its own right, so this mission stops at the arithmetic core, part (i), which is what
implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete
Theorem 4.3.
Two things the development established that the paper does not state. First, Lemma 2.1 is true
in a **stronger** form: $[G : A \cap B] \mid [G:A]\,[G:B]$ needs only $A$ subnormal, not both, and
needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is $0$).
Second, Theorem 4.1's passage from the largest prime $p^*$ to the smallest $p_*$ can be isolated
as a self-contained arithmetic inequality, $(p_*-1)\prod_{p\mid N}p \le p^*\prod_{p\mid N}(p-1)$,
which is tight at prime powers; it is listed as its own milestone for that reason.
Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of
Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim
including the still-open solvable case. The source also leaves **Conjecture 4.1** open — that for
a nontrivial uniform cover by subnormal subgroups the *largest* index $n$ is repeated at least
$p(n)$ times, $p(n)$ its least prime factor — which would be a natural follow-on target.
## Selected references
- Z.-W. Sun, *On the Herzog–Schönheim conjecture for uniform covers of groups*, Journal of Algebra **273** (2004) 153–175. [DOI](https://doi.org/10.1016/S0021-8693(03)00526-X)
- M. Herzog, J. Schönheim, *Research problem No. 9*, Canadian Mathematical Bulletin **17** (1974) 150.
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *The Herzog–Schönheim conjecture for finite nilpotent groups*, Canadian Mathematical Bulletin **29** (1986) 329–333. [DOI](https://doi.org/10.4153/CMB-1986-050-0)
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *Remark on the multiplicity of a partition of a group into cosets*, Fundamenta Mathematicae **128** (1987) 139–144. [DOI](https://doi.org/10.4064/fm-128-3-139-144)
- N. Burshtein, *On natural exactly covering systems of congruences having moduli occurring at most M times*, Discrete Mathematics **14** (1976) 205–214. [DOI](https://doi.org/10.1016/0012-365X(76)90033-0)
- R. J. Simpson, *Exact coverings of the integers by arithmetic progressions*, Discrete Mathematics **59** (1986) 181–190. [DOI](https://doi.org/10.1016/0012-365X(86)90372-2)
- Z.-W. Sun, *Exact m-covers of groups by cosets*, European Journal of Combinatorics **22** (2001) 415–429. [DOI](https://doi.org/10.1006/eujc.2000.0413)
- B. H. Neumann, *Groups covered by finitely many cosets*, Publicationes Mathematicae Debrecen **3** (1954) 227–242.
- L. Margolis, O. Schnabel, *The Herzog–Schönheim conjecture for small groups and harmonic subgroups*, Beiträge zur Algebra und Geometrie **60** (2019) 399–418. [arXiv](https://arxiv.org/abs/1803.03569)
16 thms1 active userReviewed
🏆Completed
Captain: burkh4rt
Herzog-Schönheim for finite pyramidal groupsResearch Paper
## Motivation
A **coset partition** of a group $G$ is a finite family of left cosets $a_1K_1, \dots, a_tK_t$ of
subgroups $K_i \le G$ that are pairwise disjoint and cover $G$. Asking which multisets of indices
$[G:K_i]$ can occur is a question with two independent origins. For $G = \mathbb{Z}$ the cosets are
arithmetic progressions and a coset partition is an **exact covering system** of the integers;
Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado,
and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For
general groups, [Herzog and Schönheim (1974)](https://doi.org/10.4153/CMB-1974-025-7) asked the
same question: in any coset partition with $t > 1$, must two of the indices coincide? That question
is still open.
Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture
for finite **nilpotent** groups in [Canad. Math. Bull. 29 (1986)
329–333](https://doi.org/10.4153/CMB-1986-050-0), and the paper formalized here extends it to a
wider class defined by a chain condition. Later work bounds the order instead of the structure:
[Ginosar and Schnabel (2011)](https://www.researchgate.net/publication/265126234) settle every $G$
whose order has at most two prime divisors, and three prime divisors when $6 \nmid |G|$, while
[Margolis and Schnabel (2019)](https://arxiv.org/abs/1803.03569) verify all $|G| < 1440$. The
conjecture remains open even for finite solvable groups.
## Setting
Let $p(m)$ denote the least prime factor of $m$ and $P(m)$ the greatest, and let $\varphi$ be
Euler's totient function.
A finite group $G$ is **pyramidal** if it admits a chain of subgroups
$$ \{1\} = G_n \subseteq G_{n-1} \subseteq \cdots \subseteq G_1 \subseteq G_0 = G $$
in which every step has index equal to the least prime factor of the order of the preceding term:
$$ [G_{k-1} : G_k] = p\!\left(|G_{k-1}|\right), \qquad 1 \le k \le n. $$
A subgroup whose index is the smallest prime dividing the order is automatically normal, so the
chain is a composition series; consequently every pyramidal group is **solvable**, and every
**supersolvable** group is pyramidal. Pyramidality is therefore a chain condition sitting between
supersolvability and solvability.
Given a coset partition $a_1K_1, \dots, a_tK_t$ of $G$, write
$$ l \;=\; \frac{|G|}{\gcd\!\left(|K_1|, \dots, |K_t|\right)} . $$
## Target
The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If $G$ is
pyramidal and the cosets $a_iK_i$, $1 \le i \le t$, partition $G$ with $t > 1$, then at least
$$ x \;=\; \left\lfloor \frac{P(l)\,\varphi(l)}{l} \right\rfloor + 1 $$
of the subgroups $K_i$ have the same order.
Two consequences are separate targets. Since $x \ge 2$ whenever $l \ge 2$, the bound yields the
**Herzog–Schönheim conjecture for pyramidal groups**:
$$ \exists\, i \ne j, \qquad [G : K_i] = [G : K_j], $$
and it likewise settles Burshtein's conjecture in this setting, which concerns the case
$\gcd(|K_i|) = 1$ and bounds the primes dividing $|G|$ in terms of the largest multiplicity.
## Significance
The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely
assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with
the largest prime factor of $l$. That is what makes it strong enough to also imply Burshtein's
conjecture, which no purely qualitative statement does.
The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result
subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from
nilpotent. It remains, more than three decades later, among the structural (as opposed to
order-bounded) cases in which the conjecture is known.
No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory,
Hall subgroups of solvable groups, Euler's totient with Gauss's identity $\sum_{d \mid m}\varphi(d)
= m$ — but neither coset partitions as a structure, nor pyramidality, nor any case of
Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the
conjecture, together with a reusable formal vocabulary for coset partitions.
## Difficulty
The reciprocal identity $\sum_i [G:K_i]^{-1} = 1$ is immediate and useless on its own: distinct
indices can satisfy it, so no counting argument over the indices alone can succeed.
The natural attack — induct along the chain, quotienting by $G_1$ — fails because a coset partition
does not descend to a quotient. A part $a_iK_i$ need not lie inside a single coset of $G_1$: if
$K_iG_1 = G$ then it meets every coset of $G_1$, and the induced family on $G/G_1$ is a cover with
multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is
precisely where the definition of pyramidality is used, the index $[G:G_1]$ being the *least* prime
factor of $|G|$ rather than an arbitrary one.
The second obstacle is that the conclusion counts subgroups of equal **order**, so the induction
must carry a lower bound on the size of a union of cosets that is sensitive to the orders $|K_i|$
and not merely to their number. The paper's device is a measure $\mu$ on the naturals with
$\mu(\{m\}) = \varphi(m)$, evaluated on the divisor closure of the set of orders; Gauss's identity
makes $\mu$ interact correctly with divisibility, and the required inequality is genuinely a
statement about the group, not about the multiset of orders. The final step splits off the Sylow
$P(|G|)$-subgroup against a Hall complement, which exists only because pyramidal groups are
solvable.
## Formalization scope
The development commits to the following conventions, all fixed in Lean and worth stating because
the prose leaves them implicit.
Coset partitions are indexed families rather than sets of cosets: `IsCosetPartition K a` asserts
that for every $x$ there is a **unique** index $i$ with $(a_i)^{-1}x \in K_i$. Indexing by `Fin t`
keeps multiplicities visible, which matters since the conclusion counts indices, not distinct
subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via
`[Finite G]`, and orders and indices are `Nat.card` and `Subgroup.index`.
Pyramidality is stated as the existence of a length $n$ and a chain `c : ℕ → Subgroup G` with
`c 0 = ⊤`, `c n = ⊥`, and `Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k))` for
`k < n`. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed.
The greatest prime factor is `maxPrimeFac m = m.primeFactors.sup id`, which is $0$ for
$m \in \{0,1\}$; the floor in $x$ is natural-number division, so the goal statement is
`(maxPrimeFac l * Nat.totient l) / l + 1 ≤ …`. Note that the bound is vacuous at $l = 1$ — there
$P(1)\varphi(1)/1 = 0$ and $x = 1$ — so $t > 1$ is a necessary hypothesis and is present in every
statement that needs it; a formalization omitting it would be trivially true and is ruled out.
A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index
dichotomy; uniqueness of the Sylow $P(|G|)$-subgroup of a pyramidal group; the scaling law
$\mu(D(kR)) = k\,\mu(D(R))$ for the divisor-closure measure; the union lower bound; and
solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable
for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions
of alternative proofs or sharper variants are welcome.
## Selected references
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *Remark on the multiplicity of a partition of a group into cosets*, Fundamenta Mathematicae **128** (1987) 139–144. [DOI](https://doi.org/10.4064/fm-128-3-139-144)
- M. A. Berger, A. Felzenbaum, A. S. Fraenkel, *The Herzog–Schönheim conjecture for finite nilpotent groups*, Canadian Mathematical Bulletin **29** (1986) 329–333. [DOI](https://doi.org/10.4153/CMB-1986-050-0)
- M. Herzog, J. Schönheim, *Research problem No. 9*, Canadian Mathematical Bulletin **17** (1974) 150.
- N. Burshtein, *On natural exactly covering systems of congruences having moduli occurring at most M times*, Discrete Mathematics **14** (1976) 205–214. [DOI](https://doi.org/10.1016/0012-365X(76)90033-0)
- I. Korec, Š. Znám, *On disjoint covering of groups by their cosets*, Mathematica Slovaca **27** (1977) 3–7.
- Z.-W. Sun, *On the Herzog–Schönheim conjecture for uniform covers of groups*, Journal of Algebra **273** (2004) 153–175. [DOI](https://doi.org/10.1016/S0021-8693(03)00526-X)
- L. Margolis, O. Schnabel, *The Herzog–Schönheim conjecture for small groups and harmonic subgroups*, Beiträge zur Algebra und Geometrie **60** (2019) 399–418. [arXiv](https://arxiv.org/abs/1803.03569)
12 thms1 active userReviewed
🏆Completed
Captain: dbenbenn
Brin–Squier: the group of piecewise-linear homeomorphisms of the line with finitely many breakpoints has no free subgroup of rank greater than oneResearch Paper
## Motivation
[Von Neumann introduced amenability in 1929](http://eudml.org/doc/211921) in response to the
Banach–Tarski paradox: a group is **amenable** when it carries a finitely additive,
translation-invariant probability measure on its subsets, and no amenable group contains a free
subgroup of rank $2$ — which is exactly what the paradox needs. The converse is the **von
Neumann conjecture**, and it is false: [Ol'shanskii](https://doi.org/10.1070/rm1980v035n04abeh001876) in 1980 and
[Adyan](https://doi.org/10.1070/im1983v021n03abeh001799) in 1982 produced finitely generated
counterexamples. A *finitely
presented* counterexample was harder, and one candidate stood out — **Richard Thompson's group
$F$**, finitely presented, with nobody able to decide whether it was amenable.
Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that
$F$, and more generally the group $\mathrm{PLF}(\mathbb{R})$ of piecewise-linear homeomorphisms
of the line with finitely many breakpoints, contains no free subgroup of rank greater than $1$.
Whether $F$ is amenable they could not determine, and it is still open today; claimed proofs
have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes
([Ol'shanskii–Sapir 2002](https://doi.org/10.1007/s10240-002-0006-7);
[Lodha–Moore 2016](https://doi.org/10.4171/ggd/347)), so $F$
is no longer needed as a candidate. This mission formalizes the half that *was* settled.
## Setting
Let $\mathrm{Homeo}_+(\mathbb{R})$ be the **group of orientation-preserving homeomorphisms** of
the line: the strictly increasing bijections $\mathbb{R}\to\mathbb{R}$ under composition. The
**support** of $f$ is the set of points it moves, $\operatorname{supp} f = \{\,t : f(t)\neq t\,\}$, an open subset of $\mathbb{R}$.
A continuous $f$ is **piecewise linear** when there is a *discrete* set $B$ of **breakpoints**
with $f$ differentiable off $B$ and $f'$ constant on each component of $\mathbb{R}\setminus B$;
for finite $B$ this is the same as $f$ being affine on a neighbourhood of every point outside
$B$. Nothing is required at the points of $B$, so the two affine pieces meeting at a breakpoint
may disagree — that is what makes such an $f$ more than an affine map. Write
$\mathrm{PL}(\mathbb{R})$ for the piecewise-linear elements of $\mathrm{Homeo}_+(\mathbb{R})$
and
$$\mathrm{PLF}(\mathbb{R}) = \{\, f \in \mathrm{PL}(\mathbb{R}) : f \text{ has a finite
breakpoint set} \,\}$$
for the subgroup this mission is about. The distinction matters: the goal below holds in
$\mathrm{PLF}(\mathbb{R})$ and fails in $\mathrm{PL}(\mathbb{R})$, where Brin and Squier build
free subgroups of rank $2$ by lifting them from the circle. Write $\mathrm{PLF}'(\mathbb{R})$ for the commutator subgroup, which Brin and Squier identify
as the elements whose **slope at each end** is $1$ — an element has slope $a$ at an end when it
agrees with a single affine map of slope $a$ on a ray out to that end. **Thompson's group $F$** — the piecewise-linear homeomorphisms of $[0,1]$ with dyadic
breakpoints and power-of-two slopes — is realized inside $\mathrm{PLF}(\mathbb{R})$.
## Formalization targets
### Goal — no two elements generate freely
$$\text{for } f,g \in \mathrm{PLF}(\mathbb{R}), \quad F_2 \to \mathrm{PLF}(\mathbb{R}),\
a \mapsto f,\ b \mapsto g \quad\text{is never injective.}$$
Since a free group of rank greater than $1$ contains one of rank $2$, this is Brin and Squier's
Theorem (3.1).
### The dichotomy it rests on
$$G \le \mathrm{PLF}'(\mathbb{R}) \implies G \text{ abelian, or } G \text{ contains a free
abelian subgroup of rank } 2.$$
Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is
infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the
full-strength (3.2) are milestones of their own here. The goal itself only ever uses the
rank-two form.
### The twenty-four milestones
Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in
its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and
published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2)
both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3),
likewise in both strengths. Five are piecewise-linear infrastructure the source treats as
routine: closure of $\mathrm{PLF}(\mathbb{R})$ under composition and under inverse, the same two
for slope $1$ at each end, and finiteness of the number of components of a support. Five more are
steps the source asserts without proof — that the line carries no non-fixed periodic points, that
a map fixing a set's complement preserves its components, that the iterated images of a
pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays
inside the union of the two supports (p. 495), and that the derived subgroup of a free group of
rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian
subgroup of a free group is cyclic, which is what lets the goal finish through
Nielsen–Schreier.
## Significance
The theorem closes the standard route to proving a group **non**-amenable. To show a group
amenable the classical routes are elementary amenability and subexponential growth, and $F$ is
neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth,
having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route
is to exhibit a free subgroup of rank $2$ — the route this theorem closes. $F$ sits in the gap,
which is why its status has survived sustained attention.
The result reaches past $F$. Monod's groups of piecewise *projective* homeomorphisms are
counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no
non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the
corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof
that paper says it will "largely follow [Brin–Squier, § 3]".
**What formalizing it adds.** Mathlib has no piecewise-linear maps and no [amenability predicate for
groups](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Group/FoelnerFilter.lean). This mission builds the piecewise-linear layer: a workable $\mathrm{PLF}(\mathbb{R})$, its
closure properties, and the structure of supports.
## Difficulty
The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the
breakpoint set is what gives an element slopes at $\pm\infty$ at all, and what makes two elements
affine on each side of a common fixed point. Compactness is the other — throughout, $[f,g] = fgf^{-1}g^{-1}$ — and it splits: that the closure of $\operatorname{supp}[f,g]$ is
compact needs only slope $1$ at each end, with no piecewise linearity at all, which is why
(2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays
inside $\operatorname{supp} f \cup \operatorname{supp} g$ is what reaches back to finiteness. Keeping straight which
fact does which job is most of the work.
The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that
makes them commute: only their intersections with one chosen component are disjoint, and
commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.
## Formalization scope
**What the Lean fixes.** Elements are order isomorphisms of $\mathbb{R}$ — strictly increasing
bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows
Mathlib's convention $(f\cdot g)(x) = f(g(x))$, the opposite of the source's right action, so the
conjugation identity reads $\operatorname{supp}(fgf^{-1}) = f(\operatorname{supp} g)$ here;
getting this backwards states a different theorem that still compiles. A support is the bare
moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with
local affineness off it — the set need not be minimal and may be empty.
A copy of $\mathbb{Z}^2$ is an injectivity statement about $(m,n)\mapsto u^m v^n$, not a subgroup
isomorphism, and the goal is about a single pair $f,g$ rather than a subgroup. The dichotomy
hypothesises slope $1$ at both ends directly, not membership in a derived subgroup — that these
coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and
the identification asserted on p. 493 gives the other.
Beyond a workable $\mathrm{PLF}(\mathbb{R})$, the development needs Nielsen–Schreier, already
in Mathlib as `subgroupIsFreeOfIsFree`: it is what lets an abelian subgroup of a free group be
cyclic, and so lets the goal finish without the source's metabelian ending. That ending is
formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a
free group of rank two is non-abelian; the goal simply does not route through it.
**One trivializing reading is ruled out.** Slope $1$ at both ends is not a compact-support
condition — every translation satisfies it — so (3.2) is not secretly a statement about
compactly supported maps.
**Nothing is built for $F$ specifically**, and amenability is not touched. That is the one piece
deliberately omitted, and contributions are welcome on it: modelling $F$ and embedding it in
$\mathrm{PLF}(\mathbb{R})$. The piecewise-linear layer is reusable beyond this theorem — Thompson's groups $T$ and
$V$, and piecewise-linear topology generally, need exactly it.
## Selected references
- M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line,
Invent. math. **79** (1985), 485–498, [doi:10.1007/BF01388519](https://doi.org/10.1007/BF01388519). Theorem (3.1) is the goal.
- J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups,
L'Enseignement Mathématique **42** (1996), 215–256. Theorem 4.10 and Corollary 4.7.
- N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA **110**
(2013), 4524–4527, [arXiv:1209.5229](https://arxiv.org/abs/1209.5229).
- A. Yu. Ol'shanskii and M. V. Sapir, Non-amenable finitely presented torsion-by-cyclic groups,
Publ. Math. IHÉS **96** (2002), 43–169, [doi:10.1007/s10240-002-0006-7](https://doi.org/10.1007/s10240-002-0006-7).
- Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective
homeomorphisms, Groups Geom. Dyn. **10** (2016), 177–200, [doi:10.4171/ggd/347](https://doi.org/10.4171/ggd/347).
- V. Guba, Amenability problem for Thompson's group $F$: state of the art, J. Groups Complex.
Cryptol. **15** (2023), [arXiv:2305.07113](https://arxiv.org/abs/2305.07113).