Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Corollary-Definition 2.7: the unique normal form in FFF

Proved
CannonFloydParry.existsUnique_normalForm

by dbenbenn · Sep 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgroup-theorythompsons-grouptree-diagrams

Corollary-Definition 2.7. Every element f≠1f \ne 1f=1 of Thompson's group FFF can be written in exactly one way as

f=X0b0X1b1⋯Xnbn Xn−an⋯X1−a1X0−a0f = 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}f=X0b0​​X1b1​​⋯Xnbn​​Xn−an​​⋯X1−a1​​X0−a0​​

with nnn and all aka_kak​, bkb_kbk​ nonnegative integers such that (i) exactly one of ana_nan​ and bnb_nbn​ is nonzero, and (ii) if ak>0a_k > 0ak​>0 and bk>0b_k > 0bk​>0 for some k<nk < nk<n, then ak+1>0a_{k+1} > 0ak+1​>0 or bk+1>0b_{k+1} > 0bk+1​>0.

Uniqueness is asserted of the exponent data itself: there is exactly one pair of finite lists satisfying the two conditions whose word is fff.

Preamble
import Definitions.Def_CannonFloydParry
import Definitions.Def_CannonFloydParry_Trees
import Definitions.Def_CannonFloydParry_TreeDiagrams
import Mathlib
Formal statement
namespace CannonFloydParry

theorem existsUnique_normalForm {f : UI ≃o UI} (hf : f ∈ F) (hne : f ≠ 1) :
    ∃! p : List ℕ × List ℕ, IsNormalFormData p.1 p.2 ∧ f = word p.2 * (word p.1)⁻¹ := by
  sorry

end CannonFloydParry
Source
Cannon, J. W., Floyd, W. J., Parry, W. R., Introductory notes on Richard Thompson's groups, L'Enseignement Mathematique (2) 42 (1996) 215-256, https://doi.org/10.5169/seals-87877, section 2 p. 224, Corollary-Definition 2.7
Read-back

What the Lean code literally says, in plain math · claude-opus-5

Read-back: unique normal form for a non-identity element of FFF

This is a single statement. Everything it rests on is imported, so the account below unfolds all of it; nothing needs to be looked up elsewhere.

1. The ambient group

Let I=[0,1]⊆RI = [0,1] \subseteq \mathbb{R}I=[0,1]⊆R, carrying the order inherited from R\mathbb{R}R.

By an order automorphism of III we mean a bijection g:I→Ig : I \to Ig:I→I such that for all x,y∈Ix, y \in Ix,y∈I,

x≤y  ⟺  g(x)≤g(y).x \le y \iff g(x) \le g(y).x≤y⟺g(x)≤g(y).

Such a ggg is strictly increasing, and since 000 and 111 are the least and greatest elements of III, necessarily g(0)=0g(0) = 0g(0)=0 and g(1)=1g(1) = 1g(1)=1.

Write Aut(I)\mathrm{Aut}(I)Aut(I) for the set of order automorphisms of III. It is a group under the following operations, and this is the group structure used throughout:

  • the product g⋅hg \cdot hg⋅h is the composite x↦g(h(x))x \mapsto g(h(x))x↦g(h(x)) — the left factor is applied last;
  • the identity element 111 is the identity map of III;
  • g−1g^{-1}g−1 is the inverse bijection;
  • for n∈Nn \in \mathbb{N}n∈N, gng^{n}gn is the nnn-fold composite of ggg with itself, with g0=1g^{0} = 1g0=1.

The product is associative, so unparenthesised products below are unambiguous; but the composition order above matters and is fixed as stated.

2. The subgroup FFF

Call a real number dyadic if it can be written as m/2km / 2^{k}m/2k with m∈Zm \in \mathbb{Z}m∈Z and k∈Nk \in \mathbb{N}k∈N.

Call g∈Aut(I)g \in \mathrm{Aut}(I)g∈Aut(I) admissible if there exists a finite set S⊆RS \subseteq \mathbb{R}S⊆R such that

  1. every element of SSS is dyadic, and
  2. for all x,y∈Ix, y \in Ix,y∈I with x<yx < yx<y and (x,y)∩S=∅(x,y) \cap S = \emptyset(x,y)∩S=∅ (the open interval (x,y)(x,y)(x,y) meets SSS nowhere), there exist n∈Zn \in \mathbb{Z}n∈Z and c∈Rc \in \mathbb{R}c∈R with
g(z)=2nz+cfor every z∈I with x≤z≤yg(z) = 2^{n} z + c \quad \text{for every } z \in I \text{ with } x \le z \le yg(z)=2nz+cfor every z∈I with x≤z≤y

(the closed interval, so the endpoints xxx and yyy are included even though they are themselves allowed to lie in SSS).

Note the exact shape of this: SSS is a finite set of real numbers, not required to be nonempty and not required to lie inside [0,1][0,1][0,1]; the exponent nnn ranges over all of Z\mathbb{Z}Z, so the slope 2n2^{n}2n is an arbitrary positive integer power of 222 (positive or negative exponent); and nnn and ccc may depend on the pair (x,y)(x,y)(x,y).

FFF is defined to be the smallest subgroup of Aut(I)\mathrm{Aut}(I)Aut(I) containing every admissible map: equivalently, g∈Fg \in Fg∈F if and only if ggg lies in every subgroup of Aut(I)\mathrm{Aut}(I)Aut(I) that contains all admissible maps; equivalently again, ggg is a finite product of admissible maps and inverses of admissible maps.

So the hypothesis "f∈Ff \in Ff∈F" is exactly membership in that generated subgroup. It is not the hypothesis that fff is itself admissible, although every admissible map does lie in FFF.

3. Two specific elements

Two order automorphisms of III are singled out. Each is the restriction to III of an explicitly given increasing bijection of R\mathbb{R}R which is the identity outside a bounded region; the restriction is well defined because each of those bijections carries [0,1][0,1][0,1] onto [0,1][0,1][0,1].

A(x)={x/2,0≤x≤12,x−14,12≤x≤34,2x−1,34≤x≤1.A(x) = \begin{cases} x/2, & 0 \le x \le \tfrac12, \\[2pt] x - \tfrac14, & \tfrac12 \le x \le \tfrac34, \\[2pt] 2x - 1, & \tfrac34 \le x \le 1. \end{cases}A(x)=⎩⎨⎧​x/2,x−41​,2x−1,​0≤x≤21​,21​≤x≤43​,43​≤x≤1.​ B(x)={x,0≤x≤12,x/2+14,12≤x≤34,x−18,34≤x≤78,2x−1,78≤x≤1.B(x) = \begin{cases} x, & 0 \le x \le \tfrac12, \\[2pt] x/2 + \tfrac14, & \tfrac12 \le x \le \tfrac34, \\[2pt] x - \tfrac18, & \tfrac34 \le x \le \tfrac78, \\[2pt] 2x - 1, & \tfrac78 \le x \le 1. \end{cases}B(x)=⎩⎨⎧​x,x/2+41​,x−81​,2x−1,​0≤x≤21​,21​≤x≤43​,43​≤x≤87​,87​≤x≤1.​

(The clauses agree at the shared endpoints, so both formulas are consistent; both maps fix 000 and 111, and BBB fixes all of [0,12][0,\tfrac12][0,21​] pointwise.)

4. The generators XiX_iXi​

An infinite family X0,X1,X2,…X_0, X_1, X_2, \dotsX0​,X1​,X2​,… of elements of Aut(I)\mathrm{Aut}(I)Aut(I) is defined by recursion on the index:

X0=A,Xn+1=(An)−1 B An(n∈N).X_0 = A, \qquad X_{n+1} = (A^{n})^{-1} \, B \, A^{n} \quad (n \in \mathbb{N}).X0​=A,Xn+1​=(An)−1BAn(n∈N).

With the composition convention of §1, Xn+1X_{n+1}Xn+1​ is the map x↦A−n(B(An(x)))x \mapsto A^{-n}\bigl(B(A^{n}(x))\bigr)x↦A−n(B(An(x))), i.e. the conjugate of BBB by AnA^{n}An in that order. In particular X1=(A0)−1BA0=BX_1 = (A^{0})^{-1} B A^{0} = BX1​=(A0)−1BA0=B.

5. Words

For a finite list c=(c0,c1,…,cm−1)c = (c_0, c_1, \dots, c_{m-1})c=(c0​,c1​,…,cm−1​) of natural numbers (so each ci≥0c_i \ge 0ci​≥0; the list may be empty and its length mmm is arbitrary), define

w(c)=X0 c0⋅X1 c1⋯Xm−1 cm−1∈Aut(I),w(c) = X_0^{\,c_0} \cdot X_1^{\,c_1} \cdots X_{m-1}^{\,c_{m-1}} \in \mathrm{Aut}(I),w(c)=X0c0​​⋅X1c1​​⋯Xm−1cm−1​​∈Aut(I),

with w(empty list)=1w(\text{empty list}) = 1w(empty list)=1.

Precisely: the defining recursion walks the list from its head, starting at generator index 000 and advancing the index by exactly one at each step, so the iii-th entry of the list (counting from 000) is the exponent of XiX_iXi​, and the recursion terminates with the identity element once the list is exhausted. The factors appear in the displayed order, and by §1 the leftmost factor X0c0X_0^{c_0}X0c0​​ is the one applied last. Exponents are natural numbers, so no factor Xi−1X_i^{-1}Xi−1​ can occur inside w(c)w(c)w(c); an entry ci=0c_i = 0ci​=0 contributes the identity factor.

6. The normal-form condition on a pair of lists

Let a=(a0,…,am−1)a = (a_0,\dots,a_{m-1})a=(a0​,…,am−1​) and b=(b0,…,bm′−1)b = (b_0,\dots,b_{m'-1})b=(b0​,…,bm′−1​) be finite lists of natural numbers. Throughout, an out-of-range lookup returns 000: the value at index kkk of a list is its kkk-th entry when kkk is less than the length, and is 000 for every kkk at or beyond the length.

Say the pair (a,b)(a,b)(a,b) is normal-form data when all four of the following hold.

  1. aaa is not the empty list.
  2. aaa and bbb have the same length. (With (1), both lists are nonempty; write m≥1m \ge 1m≥1 for this common length.)
  3. Looking at the final index m−1m-1m−1 of both lists, exactly one of the two entries there is zero and the other is strictly positive; formally, either
am−1=0  and  bm−1>0,oram−1>0  and  bm−1=0.a_{m-1} = 0 \ \text{ and } \ b_{m-1} > 0, \qquad \text{or} \qquad a_{m-1} > 0 \ \text{ and } \ b_{m-1} = 0.am−1​=0  and  bm−1​>0,oram−1​>0  and  bm−1​=0.

(Because of (1) the index m−1m-1m−1 is a genuine last position, and by (2) it is the last position of bbb as well, so no out-of-range lookup occurs here.) 4. For every index kkk with k+1<mk + 1 < mk+1<m — that is, every position other than the last — if ak>0a_k > 0ak​>0 and bk>0b_k > 0bk​>0, then ak+1>0a_{k+1} > 0ak+1​>0 or bk+1>0b_{k+1} > 0bk+1​>0.

Condition (4) imposes nothing at the last position and nothing beyond the end of the lists. Condition (3) is a disjunction of two conjunctions and, as written, is exclusive in effect: it cannot hold with both last entries zero, nor with both strictly positive.

These conditions are satisfiable. For instance a=(0)a = (0)a=(0), b=(1)b = (1)b=(1) is normal-form data, with (4) vacuous; for this pair w(b)⋅w(a)−1=X01⋅(X00)−1=Aw(b) \cdot w(a)^{-1} = X_0^{1} \cdot (X_0^{0})^{-1} = Aw(b)⋅w(a)−1=X01​⋅(X00​)−1=A.

7. The statement

Let fff be an order automorphism of I=[0,1]I = [0,1]I=[0,1]. Assume f∈Ff \in Ff∈F and f≠1f \ne 1f=1 (that is, fff is not the identity map of [0,1][0,1][0,1]). Then there is exactly one ordered pair (a,b)(a,b)(a,b) of finite lists of natural numbers such that

(a,b) is normal-form data, and f=w(b)⋅w(a)−1.(a,b) \text{ is normal-form data, and } \quad f = w(b) \cdot w(a)^{-1}.(a,b) is normal-form data, and f=w(b)⋅w(a)−1.

The variable fff is quantified universally over all order automorphisms of [0,1][0,1][0,1] (it is an implicit argument of the statement, but a genuine universally quantified variable). The two hypotheses are f∈Ff \in Ff∈F and f≠1f \ne 1f=1. There are no further hypotheses and no side conditions of any other kind.

Some points of precision about the conclusion.

  • The quantifier is ∃!\exists!∃!, not ∃\exists∃. Unfolded, it asserts: there exists a pair (a,b)(a,b)(a,b) satisfying both displayed conditions, and every pair (a′,b′)(a',b')(a′,b′) satisfying both displayed conditions equals (a,b)(a,b)(a,b).
  • Uniqueness is uniqueness of the pair. Since two pairs are equal exactly when their corresponding components are equal, this does determine both lists individually — both aaa and bbb are uniquely determined by fff. But it says so only jointly, among pairs satisfying both conditions at once.
  • The pair ranges over all ordered pairs of finite lists of natural numbers, with no a priori bound on length or on entries; the normal-form condition of §6 is what cuts this down, and it is part of the property being asserted-and-uniquely-determined, not a restriction on the range of the quantifier.
  • The order of the two components is as displayed: the second component bbb supplies the word on the left of the product, and the first component aaa supplies the word that is inverted on the right. With the composition convention of §1, fff is the map x↦w(b)(w(a)−1(x))x \mapsto w(b)\bigl(w(a)^{-1}(x)\bigr)x↦w(b)(w(a)−1(x)): first undo w(a)w(a)w(a), then apply w(b)w(b)w(b).
  • Nothing is asserted about f=1f = 1f=1; that case is excluded by hypothesis.

The hypotheses are jointly satisfiable, so the statement is not vacuous: AAA from §3 is admissible (take S={12,34}S = \{\tfrac12, \tfrac34\}S={21​,43​}) and hence lies in FFF, and A≠1A \ne 1A=1 because A(12)=14A(\tfrac12) = \tfrac14A(21​)=41​.

Human review
  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by dbenbenn · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, licensed under Apache 2.0.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTermsJoin SlackJoin Zulip© 2026 Prove2Me