Group Theory

This mission formalizes A. Erschler and T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155 (doi:10.1007/s00222-019-00922-0). Page and result numbers are those of arXiv:1802.09077v2.

Motivation

The growth function $v_{\Gamma,S}(n)$ of a group $\Gamma$ generated by a finite set $S$ counts the elements of word length at most $n$. A group has polynomial growth, exponential growth, or intermediate growth, strictly between the two. Grigorchuk's groups $G_\omega$ were the first groups of intermediate growth, and for forty years the precise asymptotics of their growth was open, even for the most studied of them, the first Grigorchuk group $G_{\mathbf{012}}$. Erschler and Zheng determine its growth exponent:

$$\lim_{n\to\infty}\frac{\log\log v_{G,S}(n)}{\log n} = \alpha_0,$$

where $\alpha_0 = \log 2/\log\lambda_0 \approx 0.7674$ and $\lambda_0$ is the positive root of $X^3 - X^2 - 2X - 4$. The upper bound was known; the new lower bound comes from random walks.

Timeline.

• 1980: Grigorchuk introduces the first Grigorchuk group, a finitely generated infinite periodic group (doi:10.1007/BF01078416).
• 1983: Kaimanovich and Vershik relate the Poisson boundary of a random walk to its asymptotic entropy (doi:10.1214/aop/1176993497); with Derriennic's work (Astérisque 74, 1980) this is the entropy criterion the lower bound rests on.
• 1984: Grigorchuk defines the family $G_\omega$, proves intermediate growth, and shows $\exp(cn^{1/2}) \le v_{G,S}(n) \le \exp(Cn^{\log_{32}31})$ for $G_{\mathbf{012}}$ (doi:10.1070/IM1985v025n02ABEH001281).
• 1997: Leonov raises the lower exponent to $0.504$ (Mat. Stud. 8 (1997) 192–197; no DOI).
• 1998: Bartholdi proves $v_{G,S}(n) \le \exp(Cn^{\alpha_0})$ (doi:10.1155/S1073792898000622); Muchnik and Pak prove upper bounds of this kind for more general $\omega$ in 2001 (doi:10.1142/S0218196701000450).
• 2001: Bartholdi raises the lower exponent to $0.5157$ (doi:10.1142/S0218196701000395); Brieussel's thesis (2008) reaches $0.5207$.
• 2020: Erschler and Zheng prove $v_{G,S}(n) \ge \exp(c_\epsilon n^{\alpha_0 - \epsilon})$, matching Bartholdi's upper bound.

Setting

$\mathsf T$ is the rooted binary tree, its vertices the finite words over $\{0, 1\}$ and its boundary $\partial\mathsf T$ the infinite rays; automorphisms act on the right, $x \mapsto x \cdot g$. For a string $\omega = \omega_0\omega_1\ldots \in \{\mathbf 0, \mathbf 1, \mathbf 2\}^{\mathbb N}$, the Grigorchuk group $G_\omega$ is generated by certain automorphisms of $\mathsf T$, $S = \{a, b_\omega, c_\omega, d_\omega\}$. The automorphism $a$ changes the first letter of a word, swapping the two subtrees of the root, while $b_\omega, c_\omega, d_\omega$ are defined as follows. They fix $1^\infty$, and on a word $1^k0v$ each of them either changes the first letter of $v$ or does nothing, depending on the letter $\omega_k$ of the string: if $\omega_k = \mathbf 0$, then $b_\omega$ and $c_\omega$ change it and $d_\omega$ does nothing; if $\omega_k = \mathbf 1$, then $b_\omega$ and $d_\omega$ change it and $c_\omega$ does nothing; if $\omega_k = \mathbf 2$, then $c_\omega$ and $d_\omega$ change it and $b_\omega$ does nothing. The string $\omega = (\mathbf{012})^\infty$ gives the first Grigorchuk group.

Assumption $\mathrm{Fr}(D)$ asks that every block $\omega_{kD}\ldots\omega_{kD+D-1}$ contain $\mathbf{201}$ or $\mathbf{211}$; it implies that $G_\omega$ is periodic. $L^\omega_n$ is the sum of the entries of $M_{\omega_0}\cdots M_{\omega_{n-1}}$ for three explicit $3\times 3$ matrices: the lengths of the words the substitutions of §2 produce.

A measure on a group is a function $\mu \ge 0$ of total mass 1. A function $f$ is $\mu$-harmonic if $f(x) = \sum_y f(xy)\mu(y)$, the entropy is $H(\mu) = -\sum_g \mu(g)\log\mu(g)$, and the Poisson boundary of $(\Gamma, \mu)$ is non-trivial when some bounded $\mu$-harmonic function is not constant.

Formalization targets

Goal: Theorem 8.3 (pp. 58), with the exponent the proof gives

For every $\epsilon > 0$ there is $C > 0$ such that for every $\omega$ satisfying $\mathrm{Fr}(D)$ there is a non-degenerate symmetric probability $\mu$ on $G_\omega$ of finite entropy and non-trivial Poisson boundary with, writing $l_S$ for the word length,

$$\mu\{g : l_S(g) > L^\omega_n\} \le C\,2^{-(1-\epsilon)n} \quad (n \ge 1),$$

and hence, for some $c > 0$ depending on $\omega$,

$$v_{G_\omega,S}(L^\omega_n) \ge \exp\bigl(c\,2^{(1-\epsilon)n}\bigr) \quad (n \ge 1).$$

The printed theorem has $n$ in place of $2^n$; that version is weaker and does not give the exponent.

The abstract's headline, that the volume exponent of the first Grigorchuk group is $\alpha_0$, is the last milestone, ErschlerZheng.hasVolumeExponent_firstString_alpha0: Theorem A combined with Bartholdi's upper bound.

Milestones

• §2: the entropy criterion and the Shannon theorem for random walks (Kaimanovich–Vershik, external), the Avez entropy, and Lemma 2.1: a finite-entropy measure with non-trivial boundary forces $v_{\Gamma,S}(n\phi(\varrho_n)) \ge e^{cn}$ for all large $n$.
• §3: germs of the action on $\partial\mathsf T$, the groupoid $\mathcal H(H_o)$, Fact 3.5, and Proposition 3.3: if the walk's germ at $1^\infty$ stabilizes modulo a proper subgroup, the Poisson boundary is non-trivial.
• §§2.4–2.5, 5, 7.1: the groups $G_\omega$ and their substitutions, the Schreier graph of $1^\infty$ and its Gray-code distance, cube independence, Facts 7.3–7.6 and Lemma 7.5.
• §7.2–7.6: the conjugated elements $\tilde g^v_j$ and the measures $\mu_\beta$ (Lemmas 7.7, 7.9), kernel and Green-function bounds (Propositions 7.11, 7.12, 7.18, 7.19, Lemmas 7.15–7.17, 7.21), and Theorem 7.13: $\mu_\beta$ has non-trivial Poisson boundary.
• §8: Lemma 8.1, Corollary 8.2, the goal, and after it Theorem A and the exponent of $G_{\mathbf{012}}$, with Bartholdi's upper bound as an external milestone.

Significance

The result. It answers the growth question for $G_{\mathbf{012}}$: the exponent is $\alpha_0$. It gives near-optimal lower bounds for every $G_\omega$ with $\omega$ satisfying $\mathrm{Fr}(D)$, and its measures are the first examples on these groups of random walks with non-trivial Poisson boundary and power-law tails. The method, building a measure with non-trivial boundary and controlled tail and reading off a volume bound from entropy, applies beyond Grigorchuk groups.

Formalizing it. No machine-checked proof of these results exists; Mathlib has neither Grigorchuk groups nor Poisson boundaries. On this platform the mission builds on the published bundle of the first Grigorchuk group, Garrido_Grigorchuk, from the Garrido Amenable Groups III mission, and on Chou's word balls, Chou_Growth. The general Markov-chain inputs (Cheeger, Faber–Krahn and Nash inequalities, and off-diagonal heat-kernel bounds) are separate standalone theorems.

Difficulty

Lower bounds by anti-contraction of word lengths (Grigorchuk, Leonov, Bartholdi, Brieussel) stall well below $\alpha_0$. The entropy route needs a measure with non-trivial Poisson boundary, but on a group of subexponential growth every finitely supported symmetric measure has trivial boundary. The measure must therefore have heavy tails, and the lower bound it gives is only as good as its tail decay. The difficulty is to make the tails as light as $\alpha_0$ allows while keeping the boundary non-trivial. That needs a non-homogeneous random walk on the Schreier graph of $1^\infty$ to be transient enough to fix the germ at $1^\infty$, and heat-kernel bounds for jump processes that are not translation invariant.

Formalization scope

Tree automorphisms are permutations of finite words (Garrido.BinaryTreeAut), acting on rays on the right by $x \cdot g = g^{-1}(x)$, so that $x \cdot (gh) = (x \cdot g) \cdot h$. A measure is a function $G \to \mathbb R$ summed with tsum; it is symmetric when $\mu(g^{-1}) = \mu(g)$, and non-degenerate when its support generates $G$ as a semigroup. The Poisson boundary is non-trivial (HasNontrivialPoissonBoundary) when some bounded harmonic function is not constant on the submonoid generated by the support of $\mu$; for the non-degenerate measures of the goal this is the criterion of p. 2 (ErschlerZheng.hasNontrivialPoissonBoundary_iff_exists_bounded_isHarmonic_ne_of_isNondegenerate). Growth is evaluated at real radii. The definitions are in the bundles ErschlerZheng_Walks, ErschlerZheng_Germs, ErschlerZheng_Grigorchuk and ErschlerZheng_Construction.

Where a statement departs from the print, its milestone description says so: under Correction when the printed claim is false or undefined ((2.3), the substitutions on p. 15, Fact 3.5, the Gray code on p. 34, Fact 7.3, $(\mathbf{012})^\infty \in \mathrm{Fr}(3)$ on p. 59, Lemmas 7.9, 7.17 and 7.21, Propositions 7.12 and 7.18, and the uniform digits on p. 55), and under Formalization note when it reads the print or strengthens it (Lemma 2.1, Proposition 7.19, Corollary 8.2, and the constants $\lambda_0$ and $\alpha_0$). The goal is Theorem 8.3 with the $2^n$ its proof gives, as above.

The goal is not trivial: its measure must be a non-degenerate symmetric probability on $G_\omega$, and the growth bound is about the generating set $S$ itself.

Reusable beyond this mission: Grigorchuk groups $G_\omega$ for every $\omega$ with their substitutions, germ groupoids of group actions, entropy and the Poisson boundary of random walks.

What is left out. Theorems B and C, Corollary 8.4 and the other applications in §8 to general $\omega$, which need the upper bounds of Bartholdi and Erschler (doi:10.5802/aif.2902); the side results of §§4–6 on the first Grigorchuk group (Theorem 5.7 and the critical constant of recurrence); the illustrative Examples 2.4 and 7.10; and the remarks and questions of §9. They are planned for a sequel mission.

Selected references

• A. Erschler, T. Zheng, Growth of periodic Grigorchuk groups, Invent. Math. 219 (2020) 1069–1155. doi:10.1007/s00222-019-00922-0; arXiv:1802.09077
• R. I. Grigorchuk, Burnside's problem on periodic groups, Funct. Anal. Appl. 14 (1980) 41–43. doi:10.1007/BF01078416
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985) 259–300. doi:10.1070/IM1985v025n02ABEH001281
• V. A. Kaimanovich, A. M. Vershik, Random walks on discrete groups: boundary and entropy, Ann. Probab. 11 (1983) 457–490. doi:10.1214/aop/1176993497
• Y. Derriennic, Quelques applications du théorème ergodique sous-additif, Astérisque 74 (1980) 183–201. numdam
• L. Bartholdi, The growth of Grigorchuk's torsion group, Internat. Math. Res. Notices 1998, no. 20, 1049–1054. doi:10.1155/S1073792898000622
• R. Muchnik, I. Pak, On growth of Grigorchuk groups, Internat. J. Algebra Comput. 11 (2001) 1–17. doi:10.1142/S0218196701000450
• L. Bartholdi, Lower bounds on the growth of a group acting on the binary rooted tree, Internat. J. Algebra Comput. 11 (2001) 73–88. doi:10.1142/S0218196701000395
• M. T. Barlow, A. Grigor'yan, T. Kumagai, Heat kernel upper bounds for jump processes and the first exit time, J. Reine Angew. Math. 626 (2009) 135–157. doi:10.1515/CRELLE.2009.005
• L. Bartholdi, A. Erschler, Groups of given intermediate word growth, Ann. Inst. Fourier 64 (2014) 2003–2036. doi:10.5802/aif.2902

Motivation

Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.

The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).

Setting

Let $\mathcal G$ be a finite Abelian group, written additively, with zero $\bar 0$ and order $D=|\mathcal G|$, and let $\mathcal G^+=\mathcal G-\{\bar 0\}$. For a right-hand side $g_0\in\mathcal G$, the group equation asks for nonnegative integers $t(g)$, $g\in\mathcal G^+$, with

$$\sum_{g\in\mathcal G^+}t(g)\cdot g=g_0 .$$

Its solution set is $T(\mathcal G,g_0)$; when $g_0=\bar 0$, the zero solution is excluded, as stipulated on p. 474. Each solution is a point of $\mathbb R^{\mathcal G^+}$, a space of dimension $n'=D-1$, and the master polyhedron $P(\mathcal G,g_0)$ is the convex hull of $T(\mathcal G,g_0)$. Gomory reads a solution $t$ as a path from $\bar 0$ to $g_0$ that uses the element $g$ exactly $t(g)$ times; with arc lengths $\pi(g)$ its length is $\pi\cdot t=\sum_g\pi(g)t(g)$.

An inequality $\pi\cdot t\ge\pi_0$, written $(\pi,\pi_0)$, is a face of $P(\mathcal G,g_0)$ when $\pi\ne0$, every $t\in T(\mathcal G,g_0)$ satisfies it, and the solutions on the hyperplane $\pi\cdot t=\pi_0$ generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with $\pi\cdot t=\pi_0$ are the minimal paths.

Let $\psi$ be a homomorphism of $\mathcal G$ onto a second finite Abelian group $\mathcal H$, with kernel $\mathcal K=\psi^{-1}(\bar 0)$. A coefficient vector $\pi'$ on $\mathcal H^+$ is lifted to $\mathcal G^+$ by

$$\pi(g)=\pi'(\psi g),\qquad \pi'(\bar 0)=0,$$

so that every element of the kernel gets coefficient $0$.

Formalization targets

Goal: THEOREM 19 (p. 486)

If $\psi g_0\ne\bar 0$ and $(\pi',\pi_0)$ is a face of $P(\mathcal H,\psi g_0)$ with $\pi_0>0$, then

$$\Big(\pi,\pi_0\Big),\quad \pi(g)=\pi'(\psi g),\quad\text{is a face of } P(\mathcal G,g_0).$$

For instance, the face $t_1\ge1$ of $P(\mathcal G_2,(1))$ lifts through reduction mod 2 to the face $t_1+0t_2+t_3+0t_4+t_5\ge1$ of $P(\mathcal G_6,(5))$ (p. 488).

Milestones

1. Face criterion (p. 469, proof of THEOREM 7). For $\pi_0>0$, $(\pi,\pi_0)$ is a face iff it is valid on $T$ and $n'$ linearly independent solutions satisfy $\pi\cdot t=\pi_0$.
2. Pushing paths forward (p. 486). A solution $t$ for $\mathcal G$ maps to the solution $\tau(h)=\sum_{g\in\psi^{-1}h}t(g)$ for $\mathcal H$ of the same length; hence the lifted inequality is valid.
3. Lifted minimal paths (p. 487). From a minimal path $\tau$ for $\mathcal H$ and a kernel element $k$, the path $T_k(\tau)$ is a minimal path for $\mathcal G$.
4. Rank $D-1$ (pp. 487–488). The lifted inequality has $D-1$ linearly independent minimal paths.

Further result: THEOREM 20 (p. 489)

Conversely, a face $(\pi,\pi_0)$ of $P(\mathcal G,g_0)$ with $\pi_0>0$ and $\pi(g)=0$ for some $g\ne\bar0$ is the lift of a face of $P(\mathcal H,\psi g_0)$ for some $\psi$ of $\mathcal G$ onto a group $\mathcal H$ with $\psi g=\bar 0$.

Significance

THEOREMS 19 and 20 together say that the faces of $P(\mathcal G,g_0)$ with $\pi_0>0$ and a zero coefficient are exactly the faces lifted from proper quotients of $\mathcal G$. A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for $\mathcal G_{2,2}$ and $\mathcal G_{2,2,2}$ every such face is a lift of the single nontrivial face of $P(\mathcal G_2,(1))$, and for a direct sum $\mathcal G=\mathcal K_1\oplus\mathcal K_2$ every face of the polyhedron of a summand not containing $g_0$ extends to a face for $\mathcal G$ (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.

Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.

Difficulty

Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit $D-1$ affinely independent solutions on the hyperplane, while the quotient face only supplies $|\mathcal H|-1$ of them. A solution of the quotient problem does not determine a solution for $\mathcal G$; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.

The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from $\mathcal G$-paths to $\mathcal H$-paths is a linear projection from dimension $D-1$ to $|\mathcal H|-1$ and does not lift independence by itself. It also fails at $\pi_0=0$: with $\mathcal G=\mathbb Z_6$, $\mathcal H=\mathbb Z_3$, $g_0=1$, the face $t(1)\ge0$ of $P(\mathbb Z_3,(1))$ lifts to $t(1)+t(4)\ge0$, which is valid but not a face of $P(\mathbb Z_6,(1))$.

Formalization scope

The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both $\mathcal G$ and $\mathcal H$. It commits to the following readings:

• Vectors are indexed by the subtype $\{g\mid g\ne\bar0\}$, so $\bar0$ has no coordinate and the dimension of T-space is $|\mathcal G|-1$ for each group separately; solutions are $\mathbb N$-valued, nonzero, and cast to $\mathbb R$. When $g_0\ne\bar0$, the group equation already excludes the zero vector.
• "Generated by the points on the hyperplane" means that the affine span of the tight solutions equals the hyperplane $\{x:\pi\cdot x=\pi_0\}$; $\pi\ne0$ is part of the definition and $\pi_0\ge0$ is not (THEOREM 6 proves it).
• Paths are vectors and "minimal path" means a solution with $\pi\cdot t=\pi_0$.
• $\pi'(\bar0)=0$ is built into the lift; "onto" is Function.Surjective ψ, and $g_0\notin\mathcal K$ is $\psi g_0\ne\bar0$.
• Added hypothesis $\pi_0>0$ in THEOREM 19 and the rank milestone: the page omits it, and the $\mathbb Z_6\to\mathbb Z_3$ example above shows the statement is false without it.
• The face criterion is THEOREM 7's "basic feasible solution" unfolded into $n'$ linearly independent tight solutions, stated for the master polyhedron only and for nontrivial groups, where $n'>0$.
• Pushing a path forward uses $\psi g_0\ne\bar0$, the standing hypothesis of THEOREM 19, so the pushed path cannot become the excluded zero solution.
• The lifted path $T_k(\tau)$ puts its closing $1$ on the kernel element $g_0-\sum_{g\notin\mathcal K}t_k(g)\cdot g$ itself, and adds nothing when that element is $\bar0$.
• In THEOREM 20, "nontrivial" is $\pi_0>0$, the printed $(\pi_1,\pi_0)$ is read as $(\pi,\pi_0)$, and the conclusion requires $\psi g=\bar0$ for the given zero coefficient: without it the identity map would satisfy the statement.

A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.

The development needs finite sums over fibres of $\psi$, a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of $T$, $P(\mathcal G,g_0)$ and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. doi:10.1016/0024-3795(69)90017-2
• R. E. Gomory, On the relation between integer and noninteger solutions to linear programs, Proceedings of the National Academy of Sciences 53 (1965), 260–265. doi:10.1073/pnas.53.2.260
• R. E. Gomory and E. L. Johnson, Some continuous functions related to corner polyhedra, Mathematical Programming 3 (1972), 23–85. doi:10.1007/BF01584976

Motivation

Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.

The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.

Setting

Let $\mathcal G$ be a finite Abelian group with zero $0$, and let $\mathcal G^+=\mathcal G\setminus\{0\}$. For a subset $\mathcal N\subseteq\mathcal G^+$ and a right-hand side $g_0\in\mathcal G$, a group-equation solution is a nonnegative integer vector $t\in\mathbb N^{\mathcal N}$ satisfying

$$\sum_{g\in\mathcal N}t(g)g=g_0.$$

The set of solutions is $T(\mathcal G,\mathcal N,g_0)$, and the group polyhedron $P(\mathcal G,\mathcal N,g_0)$ is their convex hull in the real coordinate space $\mathbb R^{\mathcal N}$. The master polyhedron $P(\mathcal G,g_0)$ uses $\mathcal N=\mathcal G^+$. This mission concerns $g_0\ne0$; Gomory specifies a separate convention at $g_0=0$, excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.

Gomory calls $\pi\cdot x\ge\pi_0$ a face when $\pi\ne0$, all points of $P$ satisfy the inequality, and its tight points generate the entire hyperplane $\pi\cdot x=\pi_0$ by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of $T$, which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.

Formalization targets

The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector $t$ represents a path whose total group displacement is $\sum_g t(g)g$ and whose length is $\pi\cdot t$. The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For $P(\mathcal G,g_0)$, Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.

The target is Theorem 18. Fix $g_0\ne0$ and $\pi_0>0$. With $\pi(0)=0$, system (13) is

$$\begin{aligned} \pi(g_0)&=\pi_0,\\ \pi(g)+\pi(g_0-g)&=\pi_0 &&(g\in\mathcal G^+,\ g\ne g_0),\\ \pi(g)+\pi(h)&\ge\pi(g+h) &&(g,h\in\mathcal G^+),\\ \pi(g)&\ge0 &&(g\in\mathcal G^+). \end{aligned}$$

The goal asserts the full equivalence

$$\pi\cdot x\ge\pi_0\text{ is a face of }P(\mathcal G,g_0) \quad\Longleftrightarrow\quad \pi\text{ is a basic feasible solution of (13).}$$

The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; $\pi_0$ is held fixed. Gomory 1969, pp. 481–483, Theorem 18.

Significance

Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in $|\mathcal G|-1$ coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of $P(\mathcal G,g_0)$ for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.

The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.

Difficulty

Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all $|\mathcal G|-1$ coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.

Formalization scope

Lean uses a finite Abelian group and a Finset $\mathcal N$ of nonzero elements. Its real vectors have coordinates indexed by $\mathcal N$ itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in $\mathcal G$; $P$ is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes $\mathcal N$ nonempty ($n'\ge1$), as the paper does implicitly: with no coordinates every vector would be trivially basic.

Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use $\pi(0)=0$, and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of $|\mathcal G|-1$ variables.

The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for $g_0=0$ and for other sections of the paper are outside this mission's stated domain.

Selected references

• R. E. Gomory, Some polyhedra related to combinatorial problems, Linear Algebra and Its Applications 2 (1969), 451–558. DOI: 10.1016/0024-3795(69)90017-2.

This mission formalizes 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; arXiv:1308.4250v3, whose page numbers are used): the group $G_0$ generated by three explicit piecewise projective homeomorphisms of the line is nonamenable and finitely presented, the first torsion-free finitely presented counterexample to the von Neumann–Day problem.

Motivation

A discrete group is amenable when it has a finitely additive invariant probability measure on all its subsets. A group containing a nonabelian free subgroup is not amenable, and von Neumann and Day asked whether the converse holds. The counterexamples found before Monod's work are built from torsion groups by elaborate inductive constructions. Monod (2013) found nonamenable groups without free subgroups among piecewise projective homeomorphisms of the line. Lodha and Moore isolate in Monod's group $H$ a subgroup with three explicit generators and nine explicit relations.

Timeline.

• 1929: von Neumann introduces amenability for groups (Fund. Math. 13, no DOI).
• 1950: Day poses the problem in print, attributing it to von Neumann (doi:10.1090/S0002-9947-1950-0044031-5).
• 1980: Ol'shanskii's counterexample (doi:10.1070/RM1980v035n04ABEH001876); soon after, Adyan shows certain Burnside groups are counterexamples (doi:10.1070/IM1983v021n03ABEH001799).
• 2003: Ol'shanskii and Sapir, the first finitely presented counterexample (doi:10.1007/s10240-002-0006-7); Ivanov gives another in 2005 (doi:10.1007/s10711-004-2826-8). Both are torsion-by-cyclic.
• 2013: Monod's groups $H(A)$ of piecewise projective homeomorphisms, nonamenable without free subgroups (doi:10.1073/pnas.1218426110); formalized on this platform in the Monod mission.
• 2016: Lodha and Moore, a torsion-free finitely presented counterexample (doi:10.4171/GGD/347).
• 2020: Lodha, a nonamenable group of type $F_\infty$ in the same family (doi:10.1112/topo.12172).

Setting

The generators act on the real line: $a(t) = t + 1$, and $b$, $c$ are the piecewise projective maps of p. 2 (aFun, bFun, cFun). As homeomorphisms of the projective line $\mathbb R \cup \{\infty\}$ (a, b, c) they generate $G_0$ (G0), inside the group where the published Monod bundle defines $H$ (Monod.Hpp).

Lodha and Moore move to infinite binary sequences through the continued-fraction map $\Phi$ (Phi), under which $a$, $b$, $c$ become functions $x$, $x_1$, $y_{10}$ of sequences (Proposition 3.1). There $x_s$ and $y_s$ are $x$ and $y$ acting on the sequences that extend $s$. $G$ is the group generated by all $x_s$ and $y_s$, $G_0$ the group generated by the $x_s$ and the $y_s$ with $s$ not constant, and $R$ the five families of relations (1)–(5) among them. Products are taken left to right, as in the paper.

Section 5 rewrites words in the generators by explicit substitutions into standard forms and sufficiently expanded standard forms, and tracks them through strings in $0$, $1$, $y$, $y^{-1}$; these notions form the second definitions bundle.

Formalization targets

Goal: Theorem 1.1

$$\neg\,\text{IsAmenable}(G_0) \ \wedge\ G_0 \text{ is finitely presented}.$$

Milestones

• Nonamenability (§2): Lodha and Moore's definition of a $\mu$-amenable equivalence relation, with its equivalence to amenability (Connes, Feldman and Weiss, whose theorem is published as ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel) as two milestones; Theorems 2.1 (Zimmer) and 2.2 (Carrière and Ghys) as printed; the group $K = \langle t+1, 2t, -1/t\rangle$; and the identities and orbit comparison of p. 4.
• Presentations (§3): Proposition 3.1, the identification of $a$, $b$, $c$ with $x$, $x_1$, $y_{10}$, the relations (1)–(5), the presentation of $F$ they contain, Propositions 3.4 and 3.5, the reduction to a finite presentation, the three-generator presentation of $G_0$, and Theorem 3.3.
• Section 5: Lemmas 5.2, 5.3, 5.4, 5.6, 5.9, 5.10 and 5.11.

Significance

The result. $G_0$ settles the finitely presented von Neumann–Day problem with a group that is torsion-free, has explicit generators and relations, and acts by piecewise projective maps, so its elements can be described by labeled tree diagrams much as those of Thompson's group $F$. It shows that $\langle a, b, c\rangle$ shares the combinatorics of $F$ without its unresolved amenability question.

Formalizing it. Before this mission none of the paper was formalized. The Monod mission's milestones supply the setting, and the case of Carrière and Ghys that Monod uses is already proved there by an elementary argument (Monod.not_isAmenableRel_mob).

Difficulty

Nonamenability is a short reduction to Theorem 2.2, which in general is deep. Finite presentation is the bulk: one must show that every word that evaluates to the identity can be reduced to an $X$-word by the substitutions of §5, through a well-founded ordering on standard forms (Lemma 5.6) and an analysis of how $y$ acts on binary expansions (Lemmas 5.9–5.11).

Formalization scope

Lean representation and conventions.

• Sequences are List Bool (finite) and Stream' Bool (infinite). $x$ is explicit; $y$ and $y^{-1}$ are defined by the recursion of p. 5, digit by digit.
• The groups on sequences are subgroups of the opposite of the permutation group of Stream' Bool, so that products are left to right as in the paper. Statements about $a$, $b$, $c$ take products in the opposite of the homeomorphism group for the same reason.
• a, b, c are the homeomorphisms that agree with the formulas on $\mathbb R$, and toSeqGroup turns a bijection of sequences into a group element. Both fall back to the identity for a function that is not a homeomorphism or a bijection. Every generator is in fact one, so the fallback is never reached, and a trivial group would make the goal false.
• $\phi$ is a limit of finite continued fractions; its defining equations are a milestone.
• $K$ is a subgroup of $\mathrm{PSL}_2(\mathbb R)$ (Matrix.ProjectiveSpecialLinearGroup, with the quotient topology), as on p. 4; a class acts on the projective line by the Möbius map of either of its matrices, through the published Monod bundle.

What is left out, and deviations.

• §4 (labeled tree diagrams) is not formalized: the paper calls it "not essential for understanding the proof", and its claims are left to the reader. Remark 3.2 (history) is left out, as are two remarks in the introduction: Thurston's unpublished result that $\langle a, b\rangle$ is a copy of Thompson's group $F$ (on this platform as Monod's published theorem that $H_{\mathbb Q}(\mathbb Z) \cong F$) and the assertion that $t \mapsto t + 1/2$ and $b$ generate a nonamenable group.
• Lodha and Moore's definition of a $\mu$-amenable relation is read with the action of $\mathbb Z$ Borel; read literally, every equivalence relation with countable classes would be $\mu$-amenable (the note on the definitions explains; CountableOrbit.exists_perm_rel_iff_exists_zpow_eq is the underlying fact).
• In the three-generator presentation of p. 7, the fourth and ninth relations as printed in $a$, $b$, $c$ do not hold in $G_0$ (LodhaMoorePrinted.printed_relations_four_and_nine_ne); the milestone uses the translations of the relations in $x_s$, $y_s$ that they come from.
• The substitutions of p. 9 include the rule for $y_s^{-1}$ that the proof of Lemma 5.2 uses and the paragraph before Lemma 5.6 writes out (without it Lemmas 5.2 and 5.4 fail: it is the only substitution that applies to $y_s^{-1}$, LodhaMoorePrinted.eq_of_step_singleton_y_neg_one), and allow commuting $y_u^i$ and $y_v^j$ for any exponents, as the proof of Lemma 5.6 does (with commuting only for positive exponents, Lemma 5.6 fails: LodhaMoorePosCommute.not_forall_exists_derives_sufficientlyExpanded).
• Theorems 2.1 and 2.2 and the Connes–Feldman–Weiss equivalence are cited results, stated as Lodha and Moore apply them; the direction of the equivalence from their definition to the standard one is the easy one. Both directions assume the setting of Connes, Feldman and Weiss: a $\sigma$-finite measure, quasi-invariant for the relation.

What a development needs. Monod's mission supplies $H$, its lack of free subgroups, the elementary non-amenability argument for $\mathrm{SL}_2(A)$ with $A$ dense, and the passage from an amenable group to an amenable orbit relation. The theorem of Connes, Feldman and Weiss is published and proved (ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel); it gives the hard direction of the equivalence. The presentation of Thompson's group $F$ is published by the Cannon–Floyd–Parry mission on the two presentations of Thompson's group $F$. Proofs of any milestone are welcome.

Selected references

• Y. Lodha, J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200. doi:10.4171/GGD/347
• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
• R. J. Zimmer, Amenable ergodic group actions and an application to Poisson boundaries of random walks, J. Funct. Anal. 27 (1978) 350–372. doi:10.1016/0022-1236(78)90013-7
• Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
• J. Belk, Thompson's group F, PhD thesis, Cornell University, 2004 (no DOI). arXiv:0708.3609
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877

This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups $H(A)$ of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever $A \neq \mathbf{Z}$.

Motivation

The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).

Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group $F$ with piecewise $\mathrm{PSL}_2(\mathbf{Z})$ maps of the line with rational breakpoints (p. 2). Whether $F$ is amenable is a notorious open problem, and whether $H(\mathbf{Z})$ is amenable is Monod's Problem 12 (p. 2).

Timeline

• 1914–1929. Hausdorff's paradox (1914); Banach–Tarski (1924); von Neumann introduces amenable groups (1929); Tarski characterizes amenability by the absence of paradoxical decompositions.
• 1950s. Day's classes; the question whether every non-amenable group contains a free subgroup of rank two becomes attached to von Neumann's name.
• c. 1965–1975. Thompson's groups $F$, $T$, $V$; Thurston's piecewise projective models of $F$ and $T$.
• 1979–1982. Ol'shanskii proves Tarski monsters non-amenable; Adyan does the same for free Burnside groups.
• 1985. Brin–Squier: groups of piecewise linear homeomorphisms of the line have no free subgroups.
• 2003. Ol'shanskii–Sapir: finitely presented non-amenable groups without free subgroups.
• 2013. Monod: the piecewise projective groups $H(A)$ (this paper).
• 2016. Lodha–Moore: a finitely presented subgroup of Monod's group, non-amenable and without free subgroups.

Setting

The projective line $\mathbf{P}^1$ is OnePoint ℝ, on which $\mathrm{SL}_2(A)$ acts through $\mathrm{GL}_2(\mathbf{R})$ by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring $A$ of $\mathbf{R}$ (A : Subring ℝ; $\mathbf{Z}$ is ⊥, $\mathbf{R}$ is ⊤), P A is $P_A$, the set of fixed points of hyperbolic elements (trace of absolute value greater than $2$).

A homeomorphism of $\mathbf{P}^1$ is piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $E$ (IsPiecewiseProjOn A E f) when, off some finite subset of $E$, it agrees near every point with a Möbius transformation from $\mathrm{SL}_2(A)$. Monod's $G$ (Gpp) is the group generated by the homeomorphisms piecewise in $\mathrm{PSL}_2(\mathbf{R})$, with breakpoints anywhere, and $H$ (Hpp) is its stabilizer of $\infty$ (fixInf). For a subring $A$, $G(A)$ (G A) is the subgroup of $G$ generated by its elements that are piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$ (IsPiecewiseProj A), and $H(A)$ (H A) is its stabilizer of $\infty$; $H(\mathbf{Z})$ is H ⊥. GRat is the subgroup of $G$ generated by its elements piecewise in $\mathrm{PSL}_2(\mathbf{Z})$ with breakpoints in $\mathbf{Q} \cup \{\infty\}$, and HRat its stabilizer of $\infty$: the rational-breakpoint variants of $G(\mathbf{Z})$ and $H(\mathbf{Z})$ (p. 2).

Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.

A relation $R \subseteq X \times X$ is amenable for a measure $\mu$ (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on $R$ to functions on $X$, linear up to $\mu$-null sets and invariant under the partial transformations of $R$. volP1 is the Lebesgue measure class on $\mathbf{P}^1$.

Target

The goal is Theorem 1, "The group $H(A)$ is non-amenable if $A \neq \mathbf{Z}$" (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring $A'$ of $A$, compares the orbits of $H(A')$ and $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1 \setminus \{\infty\}$ (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of $\mathrm{PSL}_2(A')$ on $\mathbf{P}^1$ is not.

The milestones are, in the paper's order: $G(A)$ consists exactly of the elements of $G$ piecewise in $\mathrm{PSL}_2(A)$ with breakpoints in $P_A$; $H = H(\mathbf{R})$; $H$ preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ($H$ has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of $H(\mathbf{Z})$ and $G(\mathbf{Z})$ with $F$ and $T$.

Significance

The result. Theorem 1 and Theorem 2 together make $H(A)$, for instance $A = \mathbf{Z}[\sqrt 2]$, a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).

Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's $F$ and $T$ (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.

Difficulty

The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in $L^\infty$, which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of $\mathrm{PSL}_2(A)$ on $\mathbf{P}^1$ is not amenable for $A$ countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in $\mathrm{SL}_2(A)$ that contradicts an invariant mean directly.

What is left out

• The second sentence of Proposition 6 (no non-trivial homomorphism from a Kazhdan group) and Proposition 8 (actions on CAT(0) spaces): property (T) and CAT(0) spaces are not in Mathlib.
• Proposition 4 ($L^2$-Betti numbers), the remarks on group laws, on the Dixmier problem and on bounded cohomology.
• Remarks 10 and 11, which discuss alternative proofs of the step taken from Carrière–Ghys.

Formalization scope

• $\mathbf{P}^1$ is OnePoint ℝ and $\mathrm{PSL}_2(A)$ acts through Matrix.SpecialLinearGroup (Fin 2) A; since $-1$ acts trivially the orbits are those of $\mathrm{PSL}_2(A)$.
• "Piecewise with finitely many pieces, each an interval" is stated locally: off a finite set of breakpoints, $f$ agrees near each point with one Möbius transformation. Pieces then extend over arcs because two Möbius maps agreeing near a point agree everywhere.
• The groups are subgroups of the homeomorphism group of OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that $G(A)$ is exactly its set of such maps and that $G = G(\mathbf{R})$.
• An amenable measured equivalence relation (p. 2) is one with a left invariant mean in the sense of Connes–Feldman–Weiss (an operator from $L^\infty$ of the relation to $L^\infty(X, \mu)$, their Definition 6), as in Schmidt, whom the paper cites. The paper describes it as a measurable assignment of means on the orbits, the motivating form in Connes–Feldman–Weiss; for that form, "an amenable group's action produces an amenable relation" is known only assuming CH. $\mathbf{P}^1$ carries its Borel σ-algebra and the Lebesgue measure class (volP1).
• "Metabelian" is the vanishing of the second derived subgroup, and "contains a free abelian group of rank two" is an injective homomorphism from $\mathbf{Z}^2$.
• Reused platform items, which solutions may import: the amenability and free-subgroup definitions (Garrido, Chou), Brin–Squier's Theorem 3.1, and Thompson's $F$ and $T$ (Cannon–Floyd–Parry).

Selected references

• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
• A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
• K. Schmidt, Algebraic ideas in ergodic theory, CBMS Regional Conference Series in Mathematics 76, AMS (1990) (a book; no DOI).
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519

This mission formalizes Geoghegan's conjecture that Thompson's group $F$ is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.

Motivation

A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group $F$ the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that $F$ is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that $F$ is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.

Timeline.

• 1965: Richard Thompson defines the groups $F$, $T$ and $V$ (Cannon–Floyd–Parry, p. 215).
• 1979: Geoghegan conjectures that $F$ contains no non-abelian free subgroup and is not amenable (Cannon–Floyd–Parry, p. 227).
• 1985: Brin and Squier prove that $F$ contains no non-abelian free subgroup (doi:10.1007/BF01388519).
• 1996: Cannon, Floyd and Parry prove, using Chou's work on elementary amenable groups, that $F$ is not elementary amenable (Theorem 4.10).
• 2009–2014: announced proofs of amenability (Shavgulidze, 2009; Moore, 2012) and of non-amenability (Akhmedov, 2009; Beklaryan, 2011; Wajnryb–Witowicz, 2014) are withdrawn by their authors or found to contain serious errors.
• 2013: Moore proves that if $F$ is amenable, its Følner sets grow at least like a tower of exponentials (doi:10.4171/GGD/201).
• 2013: Monod introduces the groups $H(A)$ of piecewise-projective homeomorphisms of the line, proves that they have no non-abelian free subgroup and are not amenable for every subring $A \ne \mathbf Z$ of $\mathbf R$, and asks whether $H(\mathbf Z)$ is amenable (Problem 12) (doi:10.1073/pnas.1218426110).
• 2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, and prove that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable (Theorem 6.4; arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
• 2017: Kaimanovich proves that random walks on $F$ with finitely supported, strictly non-degenerate step distributions have non-trivial Poisson boundary (doi:10.1017/9781316576571.013).
• 2019: Chornyi shows that $F$ is amenable if and only if its action on the dyadic rationals in $(0,1)$ is extensively amenable (arXiv:1907.01440).
• 2019: Kim, Koberda and Lodha show that large powers of two homeomorphisms of the line with overlapping supports generate a copy of $F$ (doi:10.24033/asens.2397).
• 2021: Stankov records, from Kim–Koberda–Lodha, that $H(\mathbf Z)$ contains a copy of $F$, so that amenability of $H(\mathbf Z)$ would imply amenability of $F$ (doi:10.1017/etds.2019.76).
• 2023: Monod shows that the Thompson group $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in the group $H_{\mathbf Q}(\mathbf Q)$ (doi:10.4171/ggd/883).
• 2023: Guba's survey records that "the famous problem about amenability of $F$ remains open" (doi:10.46298/jgcc.2023.15.1.11315).
• 2026: OpenAI proves that $F$ is not amenable: a Lipschitz self-map of the Hilbert ball with no approximate fixed point (Benyamini–Sternfeld), composed with a recursive colouring of dyadic partitions that $F$ transports exactly, gives a uniform lower bound on the Følner ratios of $F$. The proof comes with a Lean formalization (Thompson's group F is nonamenable, September 23, 2026, github.com/openai/math).

Setting

Let UI be the unit interval $[0,1]$. Thompson's group $F$ (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of $[0,1]$ that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational $k/2^n$ and every slope a power of $2$. It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).

A mean on a set $S$ is a function $m$ from the subsets of $S$ to $[0,\infty]$ with $m(\emptyset) = 0$, $m(A \cup B) = m(A) + m(B)$ for disjoint $A, B$, and $m(S) = 1$. A group $G$ is amenable (Garrido.IsAmenable G) when it carries a mean with $m(gA) = m(A)$ for all $g \in G$ and $A \subseteq G$, where $gA = \{ga : a \in A\}$. This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in $[0,1]$.

The milestones use four further notions, defined precisely in the definitions item and in their own statements:

• A finite set $A \subseteq G$ is $\varepsilon$-Følner for a finite $\Gamma \subseteq G$ when $\sum_{\gamma\in\Gamma}|\gamma A \mathbin{\triangle} A| < \varepsilon|A|$; by Følner's criterion, $G$ is amenable exactly when it has such sets for every $\varepsilon > 0$.
• A finitely supported probability measure $\mu$ on $G$ drives a random walk; $\mu$ is strictly non-degenerate when its support generates $G$ as a semigroup, and the walk is Liouville when every bounded $\mu$-harmonic function, $f(g) = \sum_h \mu(h) f(gh)$, is constant.
• An action of $G$ on a set $X$ is extensively amenable when the finite subsets of $X$ carry a $G$-invariant mean that, for each finite $E_0 \subseteq X$, gives full weight to the finite sets containing $E_0$.
• For a subring $A$ of $\mathbf R$, Monod's group $H(A)$ consists of the homeomorphisms of the real line that are piecewise projective, $x \mapsto (ax+b)/(cx+d)$ with $\left(\begin{smallmatrix} a & b \\ c & d \end{smallmatrix}\right) \in \mathrm{SL}_2(A)$, with finitely many breakpoints, each a fixed point of a hyperbolic element of $\mathrm{SL}_2(A)$. $H_B(A)$ allows breakpoints in a set $B$ instead; $H_{\mathbf Q}(\mathbf Z)$ is isomorphic to $F$ (Thurston). A subgroup $K$ of $J$ is co-amenable when $J/K$ carries a $J$-invariant mean.

Formalization targets

Goal: Geoghegan's conjecture

$$\neg\,\mathrm{IsAmenable}(F).$$

The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.

Landmarks

The milestones are results from the literature, stated as their sources state them: $F$ has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of $F$; Kaimanovich's theorem that random walks on $F$ with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of $F$ as extensive amenability of its action on the dyadic rationals; Stankov's embedding of $F$ into Monod's $H(\mathbf Z)$; Monod's theorem that $H_{\mathbf Q}(\mathbf Z) \cong F$ is not co-amenable in $H_{\mathbf Q}(\mathbf Q)$; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.

A second open statement

Monod's Problem 12 asks whether $H(\mathbf Z)$ is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of $\mathbf R$, namely $\mathbf Z$; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of $H(\mathbf Z)$ on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of $H(\mathbf Z)$ also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).

Significance

The result. A proof of the conjecture would make $F$ a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make $F$ an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.

Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.

Difficulty

The obstructions to amenability that settle the question for most groups are absent here: $F$ has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of $F$ is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on $F$ are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.

Formalization scope

Lean representation and conventions.

• $F$ is a subgroup of the order isomorphisms of UI; $H(A)$ and $H_B(A)$ are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, $(fg)(x) = f(g(x))$; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.
• Means take values in $[0,\infty]$; total mass $1$ and finite additivity keep every value in $[0,1]$.
• Extensive amenability is stated for an action on $[0,1]$ relative to the set of dyadic rationals in $(0,1)$; the statement of Chornyi's corollary includes that $F$ maps this set to itself.
• The goal cannot be satisfied vacuously: amenability is a single existential statement about means on $F$, and $F$ is a fixed, nontrivial, finitely generated group.

What is left out.

• The Poisson boundary is not formalized: "Liouville" is Kaimanovich's equivalent reformulation through bounded harmonic functions on $\operatorname{sgr}\mu$ (p. 8).
• The "in particular" clause of Moore's Theorem 1.1, on the Følner function, is not stated separately; with Følner's criterion it follows from the stated bound.
• The withdrawn and disputed proofs in the timeline are not formalized.

What a development needs. Thompson's group $F$ and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism $H_{\mathbf Q}(\mathbf Z) \cong F$ (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.

Selected references

• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985) 485–498. doi:10.1007/BF01388519
• J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013) 633–651. doi:10.4171/GGD/201
• V. A. Kaimanovich, Thompson's group F is not Liouville, in Groups, Graphs and Random Walks, LMS Lecture Note Ser. 436 (2017) 300–342. doi:10.1017/9781316576571.013
• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• K. Juschenko, N. Matte Bon, N. Monod, M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219. doi:10.1017/etds.2016.32
• M. Chornyi, Superharmonic functions on the Lamplighter graph of Thompson's group F, preprint (2019). arXiv:1907.01440
• V. Guba, Amenability problem for Thompson's group F: state of the art, J. Groups Complex. Cryptol. 15 (2023), no. 1. doi:10.46298/jgcc.2023.15.1.11315
• S.-h. Kim, T. Koberda, Y. Lodha, Chain groups of homeomorphisms of the interval, Ann. Sci. Éc. Norm. Supér. (4) 52 (2019) 797–820. doi:10.24033/asens.2397
• B. Stankov, Non-triviality of the Poisson boundary of random walks on the group H(ℤ) of Monod, Ergodic Theory Dynam. Systems 41 (2021) 1160–1189. doi:10.1017/etds.2019.76
• OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint (September 23, 2026). github.com/openai/math
• N. Monod, Some comments on piecewise-projective groups of the line, Groups Geom. Dyn. 19 (2025) 459–476. doi:10.4171/ggd/883

This mission formalizes §6 of J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique (2) 42 (1996) 215–256, doi:10.5169/seals-87877: the definition of Thompson's group $V$ and Thompson's proof that $V$ is simple.

Motivation

Thompson's groups $T$ and $V$, introduced in unpublished notes of Richard Thompson in 1965, were the first known examples of infinite, finitely presented, simple groups. The notes of Cannon, Floyd and Parry were written in part "to make available Thompson's unpublished proofs … of the simplicity of $T$ and $V$" (p. 216); §6 is the proof for $V$.

$V$ contains $T$, which contains $F$. Earlier missions on this platform formalize $F$ and its commutator subgroup (§1 and §4), its tree-diagram normal form (§2), its presentations (§3), and the simplicity of $T$ (§5). Unlike $T$, the elements of $V$ need not be continuous: they cut the circle into pieces and rearrange them in any order, so $V$ contains every finite symmetric group.

Setting

The circle $S^1$ is $[0,1]$ with its endpoints identified, in Lean UnitAddCircle ($\mathbb{R}/\mathbb{Z}$); $[x]$ denotes the image of $x \in \mathbb{R}$. Maps compose right to left, $(fg)(t) = f(g(t))$, and $[x, y] = xyx^{-1}y^{-1}$.

The group $V$ (p. 240) consists of the right-continuous bijections of $S^1$ that map images of dyadic rationals to images of dyadic rationals, are differentiable except at finitely many images of dyadic rationals, and are linear with slope a power of $2$ on each maximal interval of differentiability. In Lean a permutation $f$ of the circle satisfies IsThompsonV f when it maps dyadic points to dyadic points and, for a finite set of dyadic breakpoints, is $[z] \mapsto [2^n z + c]$ on each half-open piece between consecutive breakpoints modulo $1$. V is the subgroup generated by these maps; that they already form a group is the first milestone.

The elements. $A$, $B$, $C$ are $T$'s generators, and $\pi_0$ (mapPi0) exchanges $[0, \tfrac12)$ and $[\tfrac12, \tfrac34)$ by $x \mapsto x/2 + \tfrac12$ and $x \mapsto 2x - 1$. The words $X_0 = A$, $X_n = A^{-(n-1)}BA^{n-1}$, $C_n = A^{-(n-1)}CB^{n-1}$, $\pi_1 = C_2^{-1}\pi_0C_2$ and $\pi_n = A^{-(n-1)}\pi_1A^{n-1}$ (p. 241) are defined once, as words in four symbols, and read both as maps of the circle and in $V_1$.

The presented group $V_1$ (p. 242) is the free group on $A$, $B$, $C$, $\pi_0$ modulo fourteen relators: the six relators of $T_1$ (§5), and eight more involving the $\pi_n$, such as $\pi_1^2$, $(\pi_2\pi_1)^3$ and $(\pi_1C_2)^3$. In $V_1$, $\Pi(n)$ is the subgroup generated by $\pi_0, \dots, \pi_{n-1}$, $\Pi = \bigcup_n \Pi(n)$, and an element is positive when it is a product of nonnegative powers of the $X_i$.

Target

The goal is the sentence in which the notes state what §6 does, "In §6 we define $V$ and give Thompson's proof that $V$ is simple" (p. 216):

$$V \text{ is simple.}$$

The route is the section's own. Lemma 6.1 shows that $A$, $B$, $C$, $\pi_0$ generate $V$ and satisfy the fourteen relations, so $V_1$ maps onto $V$. Lemmas 6.2–6.8 establish how the $\pi_i$ move past the $X_j$ and $C_n$, leading to Theorem 6.9, $V_1$ is simple, and hence $V_1 \cong V$. The goal follows.

Significance

The result. $V$ is the third of Thompson's groups and the one whose elements rearrange pieces of the circle: it is infinite, finitely presented and simple, and it contains every finite group (through the finite symmetric groups). Together with $T$ it gave the first examples of infinite finitely presented simple groups.

Formalizing it. No machine-checked proof that $V$ is simple exists on this platform, and Mathlib has nothing on Thompson's groups. This mission reuses the formalization of $F$ and $T$: $V_1$'s first six relators are $T_1$'s, and the proof of Theorem 6.9 applies Theorem 5.7 and Theorem 5.8 inside $V_1$.

Difficulty

The central difficulty is the generation half of Lemma 6.1. The notes' proof uses tree diagrams with labelled leaves: every element of $V$ permutes the intervals of one standard dyadic partition onto those of another, $F$ moves any partition to a standard comb, and the subgroup generated by $\pi_0$ and $C_{n-2}$ acts as the full symmetric group on the comb's intervals. Each step is stated in one sentence; the milestones make each a separate statement.

The algebra of $V_1$ (Lemmas 6.2–6.6) is a chain of inductions. The proofs lean on two facts the notes use without isolating them: that $T_1$ maps to $V_1$ (so §5's lemmas hold in $V_1$), and the normal form $g = p\pi C_n^m q^{-1}$ in $V_1$, stated inside the proof of Theorem 6.9. Both are milestones here. The notes also cite two facts about the finitary symmetric group $\Sigma$ without proof, its presentation and the behaviour of its proper quotients, and deduce $\Pi \cong \Sigma$; the proof of Theorem 6.9 uses all three, and each is a milestone.

What is left out

• Figures 16–19, tree-diagram computations for relations 11) and 12); the relations are stated directly in Lemma 6.1.

Formalization scope

• $V$ is a Subgroup (Equiv.Perm UnitAddCircle) generated by IsThompsonV. Half-open pieces make every element right-continuous; "linear" is read modulo $1$, so a piece may wrap past $[0]$, as a rotation does. Unlike $T$, no lift to the line is available, since elements of $V$ need not be monotone.
• $V_1$ is Mathlib's PresentedGroup on the four-element type FormalV. Relators are written out as $xyx^{-1}y^{-1}$.
• $\Sigma$ is SigmaPerm, the subgroup of Equiv.Perm ℕ of permutations moving finitely many points, and $s_i$ is the transposition of $i$ and $i + 1$; its presentation is a PresentedGroup on ℕ. $\Pi$ is taken as the subgroup of $V_1$ generated by all the $\pi_i$, which is the union of the $\Pi(n)$.
• Lemma 6.1's surjection and the isomorphism $V_1 \cong V$ pin the images of the four symbols, so no isomorphism ignoring the generators satisfies them.
• Reused platform theorems, which solutions may import: Theorem 3.4, Corollary 2.6, Lemma 4.2, Theorem 4.11, and from §5 Lemma 5.2, Lemmas 5.5 and 5.6, Theorem 5.7 and Theorem 5.8. The standard dyadic partitions of the tree-diagram milestone are the §2 bundle's IsStandardDyadicPartition.

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, §6 pp. 240–248. doi:10.5169/seals-87877