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: the commutator subgroup is simple, $F$ is not elementary amenable) and its tree-diagram normal form (§2). 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), 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
• K. S. Brown, R. Geoghegan, An infinite-dimensional torsion-free $FP_\infty$ group, Inventiones Math. 77 (1984) 367–381. doi: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