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, §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 — §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].