Wolf: growth of finitely generated solvable groupsResearch Paper
## Motivation
This mission formalizes the group theory of J. A. Wolf's *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)), namely its §3 and §4. Wolf
opens with the object of study: "If a group $\Gamma$ is generated by a finite subset $S$, then one
has the 'growth function' $g_S$, where $g_S(m)$ is the number of distinct elements of $\Gamma$
expressible as words of length $\le m$ on $S$" (p. 421). Section 3 proves that a group with a
finitely generated nilpotent subgroup of finite index "is of polynomial growth, and in fact
$c_1m^{E_1(\Delta)} \le g_S(m) \le c_2m^{E_2(\Delta)}$"; section 4 proves 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).
Applying Milnor's companion note, which is the complete mission
[Milnor: growth of finitely generated solvable groups](https://prove2.me/missions/Milnor%3A%20growth%20of%20finitely%20generated%20solvable%20groups)
on this platform, Wolf concludes "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" (p. 421). That is the Milnor–Wolf theorem,
the goal here, and Wolf's Theorem 4.8. It prompted the question Wolf asks on p. 422, "whether every
finitely generated group $\Gamma$, which is not of exponential growth, necessarily has a nilpotent
subgroup of finite index"; Grigorchuk's groups of intermediate growth
([1984](https://doi.org/10.1070/IM1985v025n02ABEH001281)) answered it in the negative, and Gromov
([1981](https://doi.org/10.1007/BF02698687)) proved that polynomial growth alone does force a
nilpotent subgroup of finite index.
## Setting
**Growth.** For a finite subset $S$ of a group $\Gamma$, the **growth function** $g_S(m)$ counts
the elements expressible as words of length $\le m$ on $S$, a word $s_1^{a_1} \cdots s_r^{a_r}$
having length $|a_1| + \cdots + |a_r|$ (p. 426). The published `MilnorWolf.growthFunction S m` takes
this as the size of the ball `Chou.wordBall S m`, the set of products of at most $m$ factors from
$S \cup S^{-1}$. Wolf's two kinds of bound (p. 421) are **polynomial growth of degree $\le E$**,
$g_S(m) \le c \cdot m^E$, and **exponential growth**, $u \cdot v^m \le g_S(m)$ with $v > 1$; the
published predicates are `MilnorWolf.HasPolynomialGrowthOfDegreeLE` and
`Chou.HasExponentialGrowth`, the latter with $u = 1$, which is what Theorem 4.3 actually produces.
Both quantify over some finite generating set, and Wolf shows (p. 427, p. 434) that neither depends
on which one.
**Growth exponents.** For a finitely generated nilpotent $\Delta$ with lower central series
$\Delta = \Delta_0 \supseteq \Delta_1 \supseteq \cdots \supseteq \Delta_{s+1} = \{1\}$, each factor
$\Delta_k/\Delta_{k+1}$ is finitely generated abelian with free part of rank $n_k$; Wolf's (3.3)
sets $E_1(\Delta) = \sum_k (k+1)n_k$ and $E_2(\Delta) = \sum_k 2^kn_k$. These are
`MilnorWolf.growthExponentOne` and `MilnorWolf.growthExponentTwo`.
**Polycyclic groups.** A solvable group is **polycyclic** if it satisfies condition (1) of
Proposition 4.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" (p. 433), where a normal series, as in Kurosh, has each term normal in
the preceding one. This is `MilnorWolf.IsPolycyclic`. **Solvable** is Mathlib's
`Group.IsSolvable`.
## Formalization targets
The goal is Wolf's Theorem 4.8 (p. 438): "Let $\Gamma$ be a finitely generated solvable group. If
$\Gamma$ has a nilpotent subgroup $\Delta$ of finite index, then $\Gamma$ is polycyclic and of
polynomial growth of degree $\le E_2(\Delta)$. If $\Gamma$ does not have a nilpotent subgroup of
finite index, then $\Gamma$ is of exponential growth."
The milestones are the results it rests on, in the paper's order. Section 3 climbs from two
rescaling lemmas (3.4, 3.5) and the growth function of a free abelian group (3.6) through generating
sets adapted to the lower central series (3.7) to the polynomial bounds for a finitely generated
nilpotent group (3.2), then passes them to a group with a finite-index subgroup (3.11). Section 4
characterises polycyclic groups (4.1, whose one hard input is Hirsch's theorem, a milestone of its
own) and proves the polycyclic dichotomy (4.3). Milnor's Theorem, already proved on this platform,
appears as a reference milestone: it is what carries 4.3 from polycyclic to solvable, and Wolf notes
on p. 437 that "J. Milnor extended the scope of Theorem 4.3 by proving [10] that a finitely
generated nonpolycyclic solvable group must be of exponential growth."
## Significance
Theorem 4.8 is the first growth dichotomy: within finitely generated solvable groups there is
nothing between polynomial and exponential, and the polynomial side is exactly the almost nilpotent
one. It is the result Gromov's theorem generalises in one direction and Grigorchuk's groups bound in
the other, and the reason a group of intermediate growth can be neither solvable nor elementary
amenable, which is how those groups were first placed outside both classes. Chou's Theorem 3.2, in
the mission
[Chou: elementary amenable groups](https://prove2.me/missions/Chou%3A%20elementary%20amenable%20groups),
extends exactly this statement to elementary amenable groups and cites both halves.
Section 3 also has independent value. The polynomial bounds with the explicit exponents $E_1$ and
$E_2$ from the lower central series are sharper than the usual textbook statement that a finitely
generated nilpotent group has polynomial growth, and the pieces along the way are reusable: the
growth function of $\mathbb Z^n$ in closed form, and the fact that polynomial growth of a given
degree is inherited from a finite-index subgroup.
## Difficulty
The hard milestone is the second half of Theorem 4.3, that a polycyclic group with no nilpotent
subgroup of finite index has exponential growth. Wolf proves it through Proposition 4.4, which
passes to a Malcev completion and reads the eigenvalues of the induced Lie algebra automorphisms;
that machinery is not in Mathlib and is not part of this mission. A route that avoids it: a
polycyclic group acts on a free abelian factor of its chain by integer matrices, so either some
element has an eigenvalue off the unit circle, and then the separation argument of Wolf's p. 437
applies verbatim with that factor in place of the Lie algebra, or every eigenvalue of every element
lies on the unit circle, and then Kronecker's theorem, which Mathlib has, makes them all roots of
unity, so a finite-index subgroup acts unipotently and is nilpotent. Wolf records in the "Added in
Proof" (p. 445) that "B. Hartley recently sent me a manuscript consisting of an alternate proof that
a polycyclic group without nilpotent subgroups of finite index is of exponential growth."
Theorem 3.2 is long rather than deep: the lower bound (3.8) and the upper bound (3.9), (3.10) are
two inductions along the lower central series, each carrying explicit word-length bookkeeping, and
both need the adapted generating sets of Lemma 3.7. Mathlib has no polycyclic groups, so
Proposition 4.1 starts from nothing; it also lacks Hirsch's theorem and P. Hall's finite
presentability results, which is why Hirsch is stated here as its own milestone rather than assumed.
## Formalization scope
No new definitions: every notion is taken from the published bundles `Chou_Growth` and
`MilnorWolf_Growth`, so the statements here are directly comparable with those of the Chou and
Milnor missions. Growth is measured on closed balls, `Chou.wordBall S m` being the products of at
most $m$ letters from $S \cup S^{-1}$ and $g_S(m)$ its cardinality, finite because $S$ is a
`Finset`. "Not of exponential growth" is the negation of an existential, so it is a statement about
every finite generating set.
Conditions (8) to (11) of Proposition 4.1, Proposition 4.4 and the Lie-theoretic apparatus of §4,
and the Riemannian geometry of §2, §5 and §6, are outside this mission; Proposition 4.1 is stated
here with its first seven conditions, which are the ones §4 uses. Hirsch's theorem is cited, not
proved, by Wolf, and appears as a milestone under its own source (Proc. London Math. Soc. 44 (1938)
53–60) rather than as an omission. Cheeger's and Hartley's sharpenings, recorded in Wolf's "Added in
Proof", are not included.
No hypothesis is vacuous: the free abelian groups witness Proposition 3.6 and Theorem 3.2, a
polycyclic group with no nilpotent subgroup of finite index exists (the semidirect product
$\mathbb Z^2 \rtimes_A \mathbb Z$ for a hyperbolic $A \in SL_2(\mathbb Z)$, which is Wolf's own
example of the exponential case), and the lamplighter group $\mathbb Z/2 \wr \mathbb Z$ is finitely
generated solvable and not polycyclic, so Theorem 4.8's second alternative is not empty either.
Contributions welcome: proofs of any milestone, and the general library results they need, such as
polycyclic groups and Hirsch's theorem.
## Selected references
- 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, *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. Milnor, *Problem 5603*, Amer. Math. Monthly 75 (1968), 685–686. The identifier is for the
Advanced Problems section 5600–5609 that contains it:
[doi:10.2307/2313822](https://doi.org/10.2307/2313822)
- K. A. Hirsch, *On infinite soluble groups. I*, Proc. London Math. Soc. 44 (1938), 53–60.
[doi:10.1112/plms/s2-44.1.53](https://doi.org/10.1112/plms/s2-44.1.53)
- A. G. Kurosh, *Theory of groups*, vol. II, 2nd ed., translated by K. A. Hirsch, Chelsea, 1955.
Scanned at
[archive.org/details/a.-g.-kurosh-the-theory-of-groups-volume-2-1960](https://archive.org/details/a.-g.-kurosh-the-theory-of-groups-volume-2-1960).
- A. I. Mal'cev, *On certain classes of infinite solvable groups*, Amer. Math. Soc. Transl. (2) 2
(1956), 1–21. [doi:10.1090/trans2/002/01](https://doi.org/10.1090/trans2/002/01)
- R. G. Swan, *Representations of polycyclic groups*, Proc. Amer. Math. Soc. 18 (1967), 573–574.
[doi:10.1090/S0002-9939-1967-0213442-5](https://doi.org/10.1090/S0002-9939-1967-0213442-5)
- 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)
- 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)
- C. Chou, *Elementary amenable groups*, Illinois J. Math. 24 (1980), 396–407.
[doi:10.1215/ijm/1256047608](https://doi.org/10.1215/ijm/1256047608)
16 thms1 active userReviewed
🏆Completed
Captain: dbenbenn
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
Captain: Lucas
Tarcha: Braid Theory and the Artin Presentation with Explicit Half-Twist GeneratorsTextbook
## Motivation
A **braid** on $n$ strands is the everyday object it sounds like: $n$ strings hanging between two
horizontal plates, each string descending monotonically, no two strings meeting. Emil Artin turned
this picture into algebra in 1925 by showing that braids form a group under concatenation and that
this group has a finite presentation with $n-1$ generators. The braid groups sit at the crossroads
of low-dimensional topology (they are the mapping class groups of punctured discs, and closures of
braids produce every link), of algebra (they are the prototypical Artin–Tits groups, torsion-free
and orderable), and of representation theory and mathematical physics through the Burau, Lawrence–
Krammer and Temperley–Lieb representations.
This mission formalizes the braid-group development of a 2023 master's dissertation, Alexsander
Andrey Gomes Tarcha's *Um Estudo Introdutório da Teoria de Tranças* (UNESP, Rio Claro), whose
capstone is Teorema 3.15: the braid group on $n$ strands admits Artin's presentation. The
dissertation builds the group structure on equivalence classes of geometric braids (Teorema 3.9),
shows that the Artin generators generate (Teorema 3.11), derives the braid and commutation
relations (Proposição 3.14), establishes the presentation (Teorema 3.15), and closes with two
structural properties: the full twist is central (Proposição 3.16) and $B_m$ embeds in $B_n$ for
$m \le n$ (Proposição 3.17).
## Setting
Work in the plane $E^2 = \mathbb{C}$. The **ordered configuration space**
$$F_{0,n}E^2 = \{(z_1,\dots,z_n) \in \mathbb{C}^n : z_k \neq z_l \text{ for } k \neq l\}$$
carries the subspace topology of $\mathbb{C}^n$, and the symmetric group $\Sigma_n$ acts on it by
permuting coordinates. The **unordered configuration space** $B_{0,n}E^2 = F_{0,n}E^2/\Sigma_n$
carries the quotient topology; its points are the $n$-element subsets of the plane. The base
configuration is $(1,2,\dots,n)$, and $*$ denotes its class in $B_{0,n}E^2$. The **geometric braid
group** is
$$\pi_1\bigl(B_{0,n}E^2, *\bigr),$$
a loop of $n$-point configurations being exactly a geometric braid, and homotopy of loops being
exactly the equivalence by elementary moves used in the dissertation.
The **elementary half-twist** $\sigma_{i+1}$, for $0 \le i \le n-2$, is the loop that rotates the
two base points $i+1$ and $i+2$ by the angle $\pi$ about their midpoint $i + \tfrac32$, leaving the
other $n-2$ points fixed:
$$t \;\longmapsto\; \Bigl\{\, i+\tfrac32 \pm \tfrac12 e^{\pi i t} \,\Bigr\} \;\cup\;
\{\,k+1 : k \neq i,\, i+1 \,\}, \qquad t \in [0,1].$$
It returns to the base configuration at $t = 1$ with the two moving points interchanged, so it is a
loop in $B_{0,n}E^2$ and defines a class in $\pi_1(B_{0,n}E^2,*)$.
The **abstract braid group** $B_n$ is the group presented by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
## Formalization targets
### Goal — Teorema 3.15, with the isomorphism pinned on generators
$$\exists\, \varphi : B_n \;\xrightarrow{\ \sim\ }\; \pi_1\bigl(B_{0,n}E^2,*\bigr), \qquad
\varphi(\sigma_{i+1}) = \bigl[\text{half-twist}_i\bigr] \ \ (0 \le i \le n-2).$$
This is the statement the dissertation actually proves: the map $\varphi$ of its proof is defined on
generators by $\varphi(x_i) = [\sigma_i]$, and the work consists in showing that it is a
well-defined homomorphism which is surjective and injective. Asking only for an abstract
isomorphism would leave the generators unconstrained; naming their images is what makes the
presentation usable downstream.
### Milestones
$$\langle\,[\text{half-twist}_i]\,\rangle = \pi_1\bigl(B_{0,n}E^2,*\bigr) \qquad \text{(Teorema 3.11)}$$
$$[\text{half-twist}_i][\text{half-twist}_j] = [\text{half-twist}_j][\text{half-twist}_i]\ (|i-j|\ge 2),
\qquad
[\text{ht}_i][\text{ht}_{i+1}][\text{ht}_i] = [\text{ht}_{i+1}][\text{ht}_i][\text{ht}_{i+1}]$$
$$\forall b \in B_2,\ \exists m \in \mathbb{Z},\ b = \sigma_1^m \qquad \text{(Proposição 3.13)}$$
$$\forall b \in B_3,\ b = \sigma_1^{a_1}\sigma_2^{b_1}\cdots\sigma_1^{a_m}\sigma_2^{b_m}
\qquad \text{(Proposição 3.14)}$$
$$(\sigma_1\sigma_2\cdots\sigma_{n-1})^n \in Z(B_n) \qquad \text{(Proposição 3.16)}$$
$$B_m \hookrightarrow B_n \ \ (m \le n) \qquad \text{(Proposição 3.17)}$$
## Significance
Artin's presentation is what makes the braid groups computable: the word problem, the Burau and
Lawrence–Krammer representations, the Markov moves on braid closures, and the Garside normal form
all start from generators and relations, while the topological side supplies the meaning of those
generators. A formalization that only exhibits an abstract isomorphism cannot be used to compute
with a given geometric braid; the version stated here transports each half-twist loop to a
generator word, which is what downstream work needs.
On the formalization side, the geometric model (configuration spaces and their fundamental groups)
and the algebraic model (a presented group) are already available on the platform in this
environment, and the abstract form of Artin's theorem is already stated there as an open problem.
What this mission adds is: the elementary half-twist as an explicit, machine-checked loop in
$B_{0,n}E^2$ — this definition is proved sorry-free here, including the injectivity of the moving
configuration at every time and the continuity of the path; the sharpened goal that fixes the
isomorphism on generators; and the dissertation's supporting results, none of which is currently
on the platform. None of the milestones or the goal has a machine-checked proof yet.
## Difficulty
Surjectivity of $\varphi$ — every braid is a product of half-twists — is a compactness-and-general-
position argument in the dissertation: cut the braid into finitely many slabs in which a single
crossing occurs. Turning that into a formal proof requires the homotopy-theoretic substitute, since
"general position" is not available for free: a loop of configurations must be subdivided and each
piece pushed to a standard crossing.
Injectivity is harder and is the step where a naive approach fails. It is not enough to check that
the relations hold; one has to know that they are *all* the relations, i.e. that a word whose braid
is null-homotopic is a consequence of the braid relations. The dissertation follows the classical
route through elementary moves on braid diagrams (its Figuras 3.22–3.26), which formalizes as a
long case analysis. The standard modern alternative is the Fadell–Neuwirth fibration together with
an induction on $n$; its inductive step needs the exact sequence of the fibration
$F_{0,n}E^2 \to F_{0,n-1}E^2$, which is itself substantial work.
## Formalization scope
The plane is $\mathbb{C}$; configurations are injective tuples indexed by `Fin n`; the unordered
configuration space is the quotient by the coordinate-permutation action with the quotient
topology; the base configuration is $(1,2,\dots,n)$ (not $(0,1,\dots,n-1)$). Braid generators are
indexed by `Fin (n-1)`, the index $i$ standing for the book generator $\sigma_{i+1}$; truncated
natural subtraction means the degenerate values $n = 0, 1$ give the trivial group, and the
statements are asserted for all $n$ including those cases. The abstract braid group is the
presented group on `Fin (n-1)` modulo the normal closure of the commutation and braid relators.
The half-twist rotates counterclockwise. The mirror symmetry $z \mapsto \bar z$ fixes the base
configuration and exchanges the two orientations, so the goal statement does not depend on this
choice; a solver may use either convention internally.
The goal cannot be satisfied trivially: it asks for a group isomorphism whose values on the
generators are the prescribed classes of explicit loops, so neither the identity on a presented
group nor an abstract counting argument suffices.
Contributions welcome beyond the milestones: the Fadell–Neuwirth exact sequence for the plane, the
pure braid group as the kernel of the map to $\Sigma_n$, the exponent-sum homomorphism, and
torsion-freeness of $B_n$. The half-twist definition published with this mission is reusable for
any further work on braids in this environment.
## Selected references
- Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, master's
dissertation, UNESP Rio Claro, 2023. https://repositorio.unesp.br/items/9d2ffbf0-8bd2-4ec7-9e45-e2cee8a1b202
- Emil Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- Joan S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
- Edward Fadell and Lee Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962),
111–118. https://doi.org/10.7146/math.scand.a-10517
42 thms5 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
Captain: Lucas
Faithfulness of the Burau representation of B4Research Paper
## Motivation
In 1935 Werner Burau attached to every braid on $n$ strands a matrix over the ring of Laurent polynomials $\mathbb{Z}[t,t^{-1}]$. The resulting homomorphism $\rho_n : B_n \to \mathrm{GL}_n(\mathbb{Z}[t,t^{-1}])$ is the oldest and most studied linear representation of the braid group, and whether it is *faithful* — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.
The history is short and sharp:
* **1969** — Magnus and Peluso prove that $\rho_3$ is faithful, by a direct algebraic computation.
* **1991** — Moody proves $\rho_n$ is **not** faithful for $n \ge 9$.
* **1993** — Long and Paton improve this to $n \ge 6$.
* **1999** — Bigelow settles $n = 5$: $\rho_5$ is not faithful.
* This left exactly one open case, $n = 4$, which appears as Question 3.1 in Margalit's problem list for mapping class groups.
* **2026** — Bharathram, Birman and Brendle prove that $\rho_4$ **is** faithful ([arXiv:2607.05283](https://arxiv.org/abs/2607.05283)), closing the last case.
## Setting
Let $n \ge 1$. The braid group $B_n$ is taken here in Artin's presentation: generators $\sigma_1,\dots,\sigma_{n-1}$ subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1}.$$
Let $R = \mathbb{Z}[t,t^{-1}]$. The **unreduced Burau representation** is the homomorphism
$$\rho_n : B_n \longrightarrow \mathrm{GL}_n(R), \qquad \sigma_i \longmapsto I_{i-1} \oplus \begin{pmatrix} 1-t & t \\ 1 & 0\end{pmatrix} \oplus I_{n-i-1},$$
i.e. the identity matrix altered only in the two rows and columns $i$, $i+1$. That these matrices satisfy the two families of braid relations — so that $\rho_n$ is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block $\begin{pmatrix} 0 & 1 \\ t^{-1} & 1-t^{-1}\end{pmatrix}$).
Equivalently, $\rho_n$ is the action of the mapping class group of the $n$-punctured disk $D_n$ on the relative homology $H_1(\widetilde{D_n}, \{\tilde p_*\})$ of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.
A representation is **faithful** when it is injective.
## Target
The goal of the mission is the Main Theorem of the paper:
$$\rho_4 : B_4 \longrightarrow \mathrm{GL}_4(\mathbb{Z}[t,t^{-1}]) \ \text{ is injective.}$$
The milestones are three supporting results, each of which can be attacked independently:
1. **Theorem 4.1 (Magnus–Peluso).** $\rho_3$ is injective. The paper gives a new topological proof of this classical statement, and the same argument is the model for the four-strand case.
2. **Observation 2.1.** If a braid $\Phi \in B_n$ satisfies $\rho_n(\Phi) = I$, then its image under the standard inclusion $B_n \hookrightarrow B_{n+1}$ (add one unbraided strand) satisfies $\rho_{n+1}(\iota(\Phi)) = I$. The paper uses this to move a four-strand braid into $B_5$, where a parity obstruction can be applied.
3. **Long's criterion** ([Long 1986, Theorem 2.2], quoted in Section 1 of the paper). If $N \trianglelefteq B_n$ is nontrivial and not contained in the centre, and $\rho_n$ is injective on $N$, then $\rho_n$ is injective. This is what reduces the Main Theorem to faithfulness on the Brunnian subgroup $\mathrm{Brun}_4$.
## Significance
Faithfulness of $\rho_4$ closes the classification of the faithful Burau representations: $\rho_n$ is faithful exactly for $n \le 4$. It immediately gives faithfulness of the Jones representation of $B_4$ (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of $\rho_n$ for $n \ge 5$ remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.
For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of $\rho_n$ over $\mathbb{Z}[t,t^{-1}]$ (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.
## Difficulty
The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for $B_4$ turns injectivity of $\rho_4$ into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how *non*-faithfulness is proved for $n \ge 5$.
The source argument is topological. To a braid $\Phi$ one associates the arc $\beta = (\beta_*^3)\Phi$ and the sequence of punctured disks cut out by its intersections with a fixed arc $\alpha$; the Moody polynomial $M(\alpha,\beta) \in \mathbb{Z}[t,t^{-1}]$ then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid $\Phi \in K_4$ into $B_5$ and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.
## Formalization scope
Conventions fixed by the Lean development:
1. $B_n$ is the abstract group given by Artin's presentation, with generators indexed by $\mathrm{Fin}(n-1)$ using truncated subtraction; the generator of index $i$ is $\sigma_{i+1}$. This is the already-published definition reused by the mission, so results proved here interoperate with other braid-group missions.
2. The representation is the **unreduced** Burau representation, of size $n \times n$, not the reduced $(n-1)$-dimensional one; the variable is written $t$ and the coefficient ring is $\mathbb{Z}[t,t^{-1}]$.
3. Faithfulness is stated as injectivity of the group homomorphism, not as triviality of the kernel on some subgroup, and it is the genuine homomorphism out of the presented group: the braid relations are verified for the Burau matrices in the definition file, so no statement here is vacuous or conditional on well-definedness.
4. Long's criterion is stated for all $n$; for $n \le 2$ its noncentrality hypothesis cannot be satisfied, so its content is the case $n \ge 3$ that the paper uses.
A complete development will additionally need: point-pushing subgroups and the Brunnian group $\mathrm{Brun}_4$, the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.
## Selected references
* V. Bharathram, J. S. Birman, T. E. Brendle, *The Burau representation is faithful for n = 4*, 2026, [arXiv:2607.05283](https://arxiv.org/abs/2607.05283).
* W. Magnus, A. Peluso, *On a theorem of V. I. Arnold*, Comm. Pure Appl. Math. 22 (1969), 683–692, [DOI:10.1002/cpa.3160220508](https://doi.org/10.1002/cpa.3160220508).
* D. D. Long, *A note on the normal subgroups of mapping class groups*, Math. Proc. Cambridge Philos. Soc. 99 (1986), 79–87, [DOI:10.1017/S0305004100063969](https://doi.org/10.1017/S0305004100063969).
* J. A. Moody, *The Burau representation of the braid group $B_n$ is unfaithful for large $n$*, Bull. Amer. Math. Soc. 25 (1991), 379–384, [DOI:10.1090/S0273-0979-1991-16080-5](https://doi.org/10.1090/S0273-0979-1991-16080-5).
* D. D. Long, M. Paton, *The Burau representation is not faithful for $n \ge 6$*, Topology 32 (1993), 439–447, [DOI:10.1016/0040-9383(93)90030-Y](https://doi.org/10.1016/0040-9383(93)90030-Y).
* S. Bigelow, *The Burau representation is not faithful for $n = 5$*, Geom. Topol. 3 (1999), 397–404, [DOI:10.2140/gt.1999.3.397](https://doi.org/10.2140/gt.1999.3.397).
7 thms2 active usersReviewed
Captain: Lucas
Braids, Links and Mapping Class Groups I: Artin's Presentation of the Braid GroupTextbook
## Motivation
The **braid group** is one of the places where group theory, low-dimensional topology and
knot theory meet. Artin introduced it in 1925 (E. Artin, *Theorie der Zöpfe*, Abh. Math. Sem.
Univ. Hamburg 4 (1925), 47–72) and returned to it in 1947; since then it has become standard
equipment in the study of links (closed braids and Markov's theorem), of mapping class groups
of punctured surfaces, and of configuration spaces. Birman's *Braids, Links, and Mapping Class
Groups* (Annals of Mathematics Studies 82, Princeton University Press, 1974) is the classical
reference that develops all three subjects from the braid group outwards, and its Chapter 1
is the foundation on which the rest of the book rests.
The chapter's structure is itself the reason to formalize it first: everything later in the
book — the closed-braid picture of links, Markov's theorem, the Magnus representations, the
mapping class group of the punctured sphere — is phrased in terms of the group
$\pi_1 B_{0,n}E^2$ and of the presentation established here. A mission that fixes faithful Lean
definitions of the configuration spaces and of the abstract braid group therefore fixes the
vocabulary for the whole series.
Timeline of the results collected here: Artin (1925) gave the presentation and the
characterization of braid automorphisms of a free group; Chow (1948) determined the centre;
Fadell–Neuwirth (1962) introduced the configuration-space fibrations, and Fadell–Van Buskirk
(1962) used them to give the proof of the presentation reproduced by Birman.
## Setting
Write $E^2$ for the Euclidean plane, identified throughout with the complex numbers $\mathbb{C}$.
For $n \ge 0$ let
$$F_{0,n}E^2 = \{\,(z_1,\dots,z_n) \in \mathbb{C}^n : z_i \neq z_j \text{ for } i \neq j\,\}$$
be the **ordered configuration space** of $n$ points in the plane, topologized as a subspace of
$\mathbb{C}^n$. The symmetric group $\Sigma_n$ acts on it by permuting coordinates; the quotient
$$B_{0,n}E^2 = F_{0,n}E^2 / \Sigma_n,$$
with the quotient topology, is the **unordered configuration space**. A point of $B_{0,n}E^2$ is
an unordered set of $n$ distinct points of the plane. The base configuration is
$\bar z^{\,0} = (1,2,\dots,n)$, and all fundamental groups below are taken at $\bar z^{\,0}$ or at
its image.
The **braid group of the plane** is $\pi_1 B_{0,n}E^2$: a loop is a motion of $n$ points of the
plane returning to the same set of points, and homotopy classes of such motions compose as
braids. The **pure braid group** is $P_n = \pi_1 F_{0,n}E^2$, the subgroup of motions returning
each point to its own starting position.
Separately, let $B_n$ denote the abstract group given by generators $\sigma_1,\dots,\sigma_{n-1}$
subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad
\sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1} \quad (1 \le i \le n-2).$$
These are equations (1-1) and (1-2) of the book (p. 11). Geometrically $\sigma_i$ interchanges the
$i$-th and $(i+1)$-st points along a semicircle.
## Formalization targets
### Goal — Theorem 1.8 (Artin, 1925; Birman p. 18)
$$B_n \;\cong\; \pi_1 B_{0,n} E^2 .$$
The group of motions of $n$ points of the plane is the group with generators
$\sigma_1,\dots,\sigma_{n-1}$ and the two families of relations above: the relations are not only
valid but *defining*.
### Milestones
The milestone list follows the chapter: the covering-space description of the projection
$F_{0,n}E^2 \to B_{0,n}E^2$ (Proposition 1.1, p. 11), the Fadell–Neuwirth exact sequence
(Theorem 1.4, p. 14), the semidirect-product decomposition of the pure braid group
(Corollary 1.8.1, p. 24), the faithful representation of $B_n$ by automorphisms of a free group
(Corollary 1.8.3, p. 25), the centre of $B_n$ (Corollary 1.8.4, p. 28, due to Chow), and Artin's
algebraic characterization of the braid automorphisms (Theorem 1.9, p. 30).
## Significance
Theorem 1.8 is what makes the braid group *computable*: with defining relations in hand one can
combine braids into the normal form of Corollary 1.8.2 and solve the word problem, represent
braids by automorphisms of a free group, and pass to the link-theoretic material of Chapters 2
and 5 where braid words, not motions, are the objects manipulated. Corollary 1.8.3 turns braids
into concrete data — a braid is determined by what it does to the generators of a free group —
and Theorem 1.9 says exactly which endomorphisms arise this way; both are the algebraic engine
behind the conjugacy-problem and Magnus-representation chapters.
For formalization the state of play is that Mathlib has free groups, presented groups, the
fundamental groupoid and fundamental group, covering maps and fibre bundles, but no braid
groups and no configuration spaces: nothing here can be assembled from existing declarations.
The mission therefore produces reusable infrastructure — configuration spaces of the plane, the
symmetric-group quotient, the Artin presentation, the Artin action on a free group — as well as
machine-checked proofs of results that are classical but, as far as the mission's search of the
library showed, not yet formalized in Mathlib.
## Difficulty
The generators and relations are easy to write down and easy to verify *in* $\pi_1 B_{0,n}E^2$;
what is hard is completeness, i.e. that no further relations are needed. The naive route —
draw the braid, push it into a normal form by hand — is exactly what a formal proof cannot do.
The Fadell–Van Buskirk argument reproduced by Birman instead runs an induction on $n$ driven by
the fibration $F_{0,n}E^2 \to F_{0,n-1}E^2$: its homotopy exact sequence gives a split extension
of $P_{n-1}$ by a free group, presentations are assembled along the extension, and finally the
covering $F_{0,n}E^2 \to B_{0,n}E^2$ with deck group $\Sigma_n$ transfers the answer from the pure
braid group to the full braid group. Each of those steps needs genuine algebraic topology —
local triviality of the projection, exactness of the homotopy sequence, freeness of
$\pi_1$ of a punctured plane — which is where the formalization work actually lies.
## Formalization scope
The plane is $\mathbb{C}$. $F_{0,n}E^2$ is the subtype of injective functions
$\mathrm{Fin}\,n \to \mathbb{C}$; $B_{0,n}E^2$ is its quotient by the equivalence "differ by
precomposition with a permutation", with the quotient topology. Base point: the configuration
$i \mapsto i+1$, i.e. $(1,2,\dots,n)$, and its image. Fundamental groups are Mathlib's
`FundamentalGroup` at those base points. Braid generators are indexed by $\mathrm{Fin}(n-1)$
with $0$-based indices ($i$ stands for $\sigma_{i+1}$), and free-group generators by
$\mathrm{Fin}\,n$; the abstract braid group is a `PresentedGroup` on that index set. Truncated
subtraction makes the generator set empty for $n \le 1$, so $B_0$ and $B_1$ are trivial, as
intended. Two milestones are stated with the shift $n \mapsto n+1$ (i.e. for the projection
$F_{0,n+1}E^2 \to F_{0,n}E^2$) to avoid truncated subtraction in the maps.
Two conventions are worth flagging because they weaken what the Lean text asserts relative to
the prose. First, the goal asserts the existence of *some* isomorphism $B_n \cong \pi_1B_{0,n}E^2$;
it does not pin the isomorphism down on the geometric generators of Figure 2, since those loops
are not part of the formal development. Second, Artin's representation is formalized as the
existence of a homomorphism $\xi$ from $B_n$ to the automorphism group of the free group whose
value on each $\sigma_i$ is the explicit endomorphism of equation (1-14), together with its
injectivity; Theorem 1.9 is then stated for an arbitrary such $\xi$, given as a hypothesis, and
is non-vacuous precisely because Corollary 1.8.3 supplies one.
No trivializing formalization is available: the goal is an isomorphism statement between two
groups that are both defined independently of it, and the degenerate cases $n \le 1$ (both sides
trivial) are genuine special cases of it, not the content.
Infrastructure a complete development needs, all reusable: freeness of $\pi_1$ of a punctured
plane, local triviality of the Fadell–Neuwirth projection, the homotopy exact sequence of a
fibration in the range needed, presentations of split extensions, and the transfer of a
presentation along a regular covering. Contributions of any of these as standalone lemmas are
welcome, as is a formalization of the geometric generators (1-9) that would let the goal be
strengthened to pin the isomorphism on $\sigma_i$.
## Selected references
- E. Artin, *Theorie der Zöpfe*, Abhandlungen aus dem Mathematischen Seminar der Universität
Hamburg 4 (1925), 47–72. https://doi.org/10.1007/BF02950718
- E. Artin, *Theory of braids*, Annals of Mathematics 48 (1947), 101–126.
https://doi.org/10.2307/1969218
- W.-L. Chow, *On the algebraical braid group*, Annals of Mathematics 49 (1948), 654–658.
https://doi.org/10.2307/1969333
- E. Fadell, L. Neuwirth, *Configuration spaces*, Mathematica Scandinavica 10 (1962), 111–118.
https://doi.org/10.7146/math.scand.a-10517
- E. Fadell, J. Van Buskirk, *The braid groups of $E^2$ and $S^2$*, Duke Mathematical Journal 29
(1962), 243–257. https://doi.org/10.1215/S0012-7094-62-02925-3
- J. S. Birman, *Braids, Links, and Mapping Class Groups*, Annals of Mathematics Studies 82,
Princeton University Press, 1974. https://doi.org/10.1515/9781400881420
39 thms5 active usersReviewed
🏆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
Captain: Lucas
The Inverse Galois ProblemOpen Problem
## Motivation
Galois theory attaches to every finite Galois extension $L/K$ a finite group $\mathrm{Gal}(L/K)$, the group of field automorphisms of $L$ fixing $K$ pointwise, and the fundamental theorem of Galois theory turns the subfield structure of $L/K$ into the subgroup structure of that group. The **inverse Galois problem** asks whether this correspondence is surjective over the rationals: given an arbitrary finite group $G$, is there a Galois extension $L/\mathbb{Q}$ with $\mathrm{Gal}(L/\mathbb{Q}) \cong G$? The question was posed in the early nineteenth century and is [unsolved](https://en.wikipedia.org/wiki/Inverse_Galois_problem).
What makes it a live research question rather than a curiosity is that the known positive results come from genuinely different sources, and none of them covers all finite groups.
- Cyclic and, more generally, finite **abelian** groups are realizable over $\mathbb{Q}$ by an explicit cyclotomic construction resting on Dirichlet's theorem on primes in arithmetic progressions.
- **Symmetric** and **alternating** groups are realizable over $\mathbb{Q}$; this is due to Hilbert, who realized them first over the rational function field $\mathbb{Q}(t)$ and then specialized $t$ using his irreducibility theorem.
- Every finite **solvable** group is realizable over $\mathbb{Q}$; this is Shafarevich's theorem (I. R. Shafarevich, *The imbedding problem for splitting extensions*, Dokl. Akad. Nauk SSSR **120** (1958), 1217–1219), obtained by solving embedding problems.
- Over $\mathbb{C}(t)$ — and over $K(t)$ for any algebraically closed $K$ of characteristic zero — *every* finite group is realizable, by the Riemann existence theorem. The obstruction to the goal is not the group theory; it is descending the field of constants to $\mathbb{Q}$.
- Case-by-case work covers large finite lists: all transitive permutation groups of degree at most $23$, and every sporadic simple group, are known to be realizable over $\mathbb{Q}$.
## Setting
Fix a field $K$ and a group $G$. A **Galois realization** of $G$ over $K$ is a field $L$ equipped with a $K$-algebra structure such that the extension $L/K$ is Galois — normal and separable — together with a group isomorphism
$$ G \;\cong\; \mathrm{Gal}(L/K), $$
where $\mathrm{Gal}(L/K)$ denotes the group of $K$-algebra automorphisms of $L$ under composition. The group $G$ is **realizable over $K$**, written `IsRealizable K G`, when at least one Galois realization of $G$ over $K$ exists. No finiteness of $L/K$ is imposed in the definition; it is automatic once $G$ is finite, because an infinite Galois extension has infinite automorphism group.
Two base fields beyond $\mathbb{Q}$ appear throughout. $K(t)$ denotes the field of rational functions in one variable over $K$, written `RatFunc K`; and for the statement that a group is realizable over *some* number field, the base field ranges over the intermediate fields of $\mathbb{C}/\mathbb{Q}$.
## Formalization targets
### Goal — the inverse Galois problem
$$ \text{for every finite group } G, \qquad \exists\, L/\mathbb{Q} \text{ Galois with } \mathrm{Gal}(L/\mathbb{Q}) \cong G. $$
The goal fixes no degree, no polynomial and no construction: it asserts only the shape of the truth, so no later refinement of the known constructions can invalidate it.
### Milestones — the known partial results
$$ G \text{ cyclic} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, \qquad G \text{ abelian} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, $$
$$ \mathrm{Sym}(S),\; A_n \text{ realizable over } \mathbb{Q}, \qquad G \text{ solvable} \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}, $$
$$ \exists\, K,\ \mathbb{Q} \subseteq K \subseteq \mathbb{C},\ G \text{ realizable over } K, $$
$$ G \text{ realizable over } \mathbb{C}(t), \qquad G \text{ realizable over } K(t) \ (K \text{ algebraically closed, char } 0), $$
$$ G \text{ realizable over } \mathbb{Q}(t) \;\Longrightarrow\; G \text{ realizable over } \mathbb{Q}. $$
The last milestone is the Hilbert-irreducibility descent step; together with the geometric milestones it makes precise which half of the classical programme is missing.
## Significance
The result itself would settle a two-century-old question and, with it, the surjectivity of the Galois correspondence over $\mathbb{Q}$: every abstract finite group would be known to arise from an explicit arithmetic object, a polynomial with rational coefficients. Its absence is felt in practice — constructing a single new Galois group over $\mathbb{Q}$ is publishable work, as the recent additions of the degree-$17$ group $17T7$ ([van Bommel–Costa–Elkies–Keller–Schiavone–Voight, 2024](https://arxiv.org/abs/2411.07857)) and of the Mathieu group $M_{23}$ show.
Formalizing it produces something available today independently of the goal: a machine-checked library of the known realizability results. Mathlib has the fundamental theorem of Galois theory, cyclotomic extensions, the Kronecker–Weber theorem, solvability of groups and symmetric/alternating group theory, but it does not have a predicate for "$G$ is a Galois group over $K$", nor any of the milestones above. Every milestone here is a *proved* theorem of classical number theory and an *unformalized* one; the cyclic and abelian cases are within reach of current Mathlib, while the Shafarevich and Riemann-existence milestones are substantial formalization projects in their own right.
## Difficulty
The obvious strategy fails at a well-understood point. Over $\mathbb{C}(t)$ the problem is solved: by the Riemann existence theorem every finite group occurs as the deck-transformation group of a branched cover of the projective line. Hilbert's irreducibility theorem then descends realizability from $\mathbb{Q}(t)$ to $\mathbb{Q}$. What is missing is the step in between: producing the cover *over $\mathbb{Q}$* rather than over $\mathbb{C}$, i.e. showing that the geometric solution can be chosen with rational field of constants. The rigidity method makes this work for many groups, but there is no known argument covering all of them; an approach that only produces realizability over some number field is not enough, and that weaker statement is included as a milestone precisely to mark the line.
A second, purely formal difficulty: the milestones are classical but their published proofs are long. Shafarevich's theorem rests on a delicate analysis of embedding problems, and the Riemann existence theorem is analytic input that Mathlib does not currently have in the required form.
## Formalization scope
The mission fixes one definition file, published first, carrying the structure `GaloisRealization` and the one-field class `IsRealizable`. Conventions it commits to:
- `IsGalois K L` is Mathlib's Galois condition (normal and separable); finiteness of the extension is *not* assumed.
- The isomorphism is with the full automorphism group $L \simeq_{\mathrm{alg}[K]} L$, not with a quotient or a subgroup of it.
- The carrier $L$ of a realization is required to live in the same universe as $K$. This costs no generality for the statements of the mission — for finite $G$ a realization is a finite extension of $K$ — and keeps every statement universe-monomorphic.
- $\mathrm{Sym}(S)$ is `Equiv.Perm S` for a finite type $S$, and $A_n$ is `alternatingGroup (Fin n)`; degenerate small cases are included rather than excluded.
- Solvability is `Group.IsSolvable`.
The statements cannot be satisfied vacuously: `IsRealizable K G` asserts the existence of data, so a solver must exhibit an extension; and the hypotheses of the milestones (cyclic, abelian, solvable, or none at all) are all satisfiable, so no milestone is empty. The one conditional milestone, Hilbert descent, is stated with realizability over $\mathbb{Q}(t)$ as an explicit hypothesis.
Infrastructure a complete development needs, most of it reusable well beyond this mission: transport of a Galois realization along an isomorphism of groups and along an isomorphism of base fields; the fixed-field construction and the fundamental theorem in the form "$\mathrm{Gal}(L/L^H) \cong H$"; Galois groups of cyclotomic fields; Dirichlet's theorem on primes in arithmetic progressions (already in Mathlib); Hilbert's irreducibility theorem (not in Mathlib). Contributions of any of these as reusable platform definitions or lemmas are welcome, as are decompositions of the harder milestones into sketches.
## Selected references
- Inverse Galois problem, *Wikipedia*. https://en.wikipedia.org/wiki/Inverse_Galois_problem
- I. R. Shafarevich, *The imbedding problem for splitting extensions*, Dokl. Akad. Nauk SSSR **120** (1958), 1217–1219.
- C. U. Jensen, A. Ledet, N. Yui, *Generic Polynomials: Constructive Aspects of the Inverse Galois Problem*, MSRI Publications 45, Cambridge University Press, 2002. http://library.msri.org/books/Book45/files/book45.pdf
- G. Malle, B. H. Matzat, *Inverse Galois Theory*, Springer Monographs in Mathematics, 1999.
- R. van Bommel, E. Costa, N. D. Elkies, T. Keller, S. Schiavone, J. Voight, *17T7 is a Galois group over the rationals*, arXiv:2411.07857, 2024. https://arxiv.org/abs/2411.07857
22 thms3 active usersReviewed
🏆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).
32 thms2 active usersReviewed
Captain: xuanji
230 space groupsTextbook
## Motivation: classify three-dimensional periodic symmetry
A **space group** describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in [Oliver Knill’s survey, §94, “Crystallography,” p. 41](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.
The target is the known classification result selected by **LeanEval v1**, not an unsolved classification conjecture. Its authoritative specification is [the declaration `LeanEval.Geometry.SpaceGroupsProblem.space_groups`](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The accompanying [benchmark manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml) attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.
## Setting: groups, transformations, and orientation
For a natural number $d$, let $E(d)=\mathbb R^d$ with its Euclidean inner product. A **Euclidean isometry** is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the [benchmark’s definitions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), $G$ is **discrete** when, for every point $x$ and every real $\varepsilon>0$, the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.
Such a group is **crystallographic** when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$. These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called `cocompact`, its actual content is the existence of these independent translations, not a separately assumed compact quotient.
An **affine equivalence** between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An **orientation-preserving affine equivalence** additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The **Sohncke subfamily** restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the [source definitions and notes](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean).
## Target: one conjunction, with all three exact counts
Write $C_{\mathrm{OP}}(d)$ for `crystallographicCountOP d`, $C(d)$ for `crystallographicCount d`, and $C_{\mathrm{OP,only}}(d)$ for `crystallographicCountOPOnly d`. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is
$$
C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.
$$
This is the [exact benchmark conjunction](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.
## Significance: exact cardinalities for the underlying groups
The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in [Knill, §94](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.
The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.
## Difficulty: a catalog is not a completeness theorem
A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the [source’s cardinality assertion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.
## Formalization scope: preserve the benchmark model
The Lean representation is `EuclideanSpace ℝ (Fin d)`, with affine isometries and affine equivalences from Mathlib. The [three source counting functions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) use `Set.encard` in the extended natural numbers $\mathbb N\cup\{\infty\}$. More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.
One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$. Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.
## Selected references
- LeanEval contributors; problem submitted by Kim Morrison. *LeanEval v1: 230 space groups*, statement revision 1, 2026, repository commit `296b7491ec989d21bcf8636a9a69231a1e5d1d25`. [Exact Lean source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean); [manifest with historical bibliography](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml).
- Oliver Knill. *Some Fundamental Theorems in Mathematics*, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. [Full text](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). This provides background for the three counts; the exact formal conventions are those of LeanEval above.