Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Every element of FFF has a reduced tree diagram

Proved
CannonFloydParry.exists_isReduced_represents

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

combinatoricsgroup-theorythompsons-grouptree-diagrams

Every fff in Thompson's group FFF is represented by some reduced tree diagram: one in which no position carries a caret in both trees, so that there is no kkk for which the kkkth and (k+1)(k+1)(k+1)th leaves of the domain tree are siblings and the kkkth and (k+1)(k+1)(k+1)th leaves of the range tree are siblings as well.

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

theorem exists_isReduced_represents {f : UI ≃o UI} (hf : f ∈ F) :
    ∃ d : TreeDiagram, IsReduced d ∧ Represents d f := 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. 221 (existence of the reduced diagram)
Read-back

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

Read-back: existence of a reduced tree diagram representing an element

The ambient objects

Throughout, III denotes the closed unit interval [0,1][0,1][0,1] of real numbers, regarded as an ordered set with the order it inherits from R\mathbb{R}R.

An order-automorphism of III is a bijection f:I→If : I \to If:I→I such that for all x,y∈Ix,y \in Ix,y∈I we have x≤yx \le yx≤y if and only if f(x)≤f(y)f(x) \le f(y)f(x)≤f(y). (The condition is required in both directions, so both fff and f−1f^{-1}f−1 are order preserving.) Such maps form a group GGG under composition: the product f⋅gf \cdot gf⋅g is the map z↦f(g(z))z \mapsto f(g(z))z↦f(g(z)), the unit is the identity map of III, and the inverse is the inverse function. Every element of GGG is strictly increasing and satisfies f(0)=0f(0)=0f(0)=0 and f(1)=1f(1)=1f(1)=1, because 000 and 111 are the least and greatest elements of III and an order isomorphism must carry each to itself.

A real number xxx is called dyadic here if there are an integer mmm and a natural number kkk with

x=m2k.x = \frac{m}{2^{k}}.x=2km​.

The integer mmm may be negative or zero, so this is the set of dyadic rationals of R\mathbb{R}R, not only those in III.

The generating property TTT

Say that f∈Gf \in Gf∈G has property TTT if there exists a finite set BBB of real numbers such that

  1. every element of BBB is dyadic, and
  2. for every pair of points x,y∈Ix,y \in Ix,y∈I with x<yx < yx<y whose open interval misses BBB, i.e. (x,y)∩B=∅(x,y) \cap B = \varnothing(x,y)∩B=∅, there exist an integer nnn and a real number ccc such that
f(z)=2nz+cfor every z∈I with x≤z≤y.f(z) = 2^{n} z + c \qquad \text{for every } z \in I \text{ with } x \le z \le y .f(z)=2nz+cfor every z∈I with x≤z≤y.

Points worth making explicit about this predicate:

  • The exponent nnn ranges over Z\mathbb{Z}Z, so the admissible slopes are exactly the integral powers of 222; in particular every slope is positive. The pair (n,c)(n,c)(n,c) may depend on xxx and yyy.
  • The affine identity is asserted on the closed interval [x,y][x,y][x,y], including its endpoints.
  • BBB is not required to be contained in III, is not required to consist of actual breakpoints of fff, and is not required to be non-empty. Conversely, condition 2 forces fff to be affine with a power-of-two slope on every subinterval of III avoiding BBB, so all genuine breakpoints of fff do lie in BBB and are therefore dyadic.
  • If BBB is empty, condition 2 applied with x=0x = 0x=0, y=1y = 1y=1 says f(z)=2nz+cf(z) = 2^n z + cf(z)=2nz+c on all of III, which together with f(0)=0f(0)=0f(0)=0 and f(1)=1f(1)=1f(1)=1 forces fff to be the identity. So the empty choice of BBB is allowed but only the identity satisfies condition 2 with it.

The group FFF

FFF is defined to be the subgroup of GGG generated by the set { f∈G:f has property T }\{\, f \in G : f \text{ has property } T \,\}{f∈G:f has property T}: the smallest subgroup of GGG containing every map with property TTT, equivalently the intersection of all subgroups of GGG that contain that set.

Consequently the assertion "f∈Ff \in Ff∈F" means: fff lies in every subgroup of GGG that contains all maps with property TTT — equivalently, fff can be written as a finite product of maps with property TTT and of inverses of such maps. It is not, as stated, the assertion that fff itself has property TTT. Having property TTT implies membership in FFF; the reverse implication is a separate claim and is not part of what is written here.

Extending a map of III to the whole line

For f∈Gf \in Gf∈G let f^:R→R\hat f : \mathbb{R} \to \mathbb{R}f^​:R→R be defined by

f^(x)={f(x),0≤x≤1,x,otherwise.\hat f(x) = \begin{cases} f(x), & 0 \le x \le 1,\\ x, & \text{otherwise.}\end{cases}f^​(x)={f(x),x,​0≤x≤1,otherwise.​

This f^\hat ff^​ is again an order isomorphism, now of R\mathbb{R}R onto itself, and it agrees with fff on III.

Finite binary trees, their leaves, and their marks

A tree here is a finite rooted binary tree built from two constructions: a single leaf, or a node formed from an ordered pair of trees (its left and right subtrees). The leaf count of a leaf is 111, and the leaf count of a node is the sum of the leaf counts of its two subtrees.

The marks of a tree ttt are a finite list of real numbers, defined by the following subdivision recursion. For a tree sss and an interval [a,b][a,b][a,b], put M(s,a,b)=M(s,a,b) =M(s,a,b)= the empty list if sss is a leaf, and, if sss is a node with left subtree ℓ\ellℓ and right subtree rrr, put

M(s,a,b)=M ⁣(ℓ,a,a+b2)  ⌢  (a+b2)  ⌢  M ⁣(r,a+b2,b),M(s,a,b) = M\!\left(\ell, a, \tfrac{a+b}{2}\right) \; \frown \; \left(\tfrac{a+b}{2}\right) \; \frown \; M\!\left(r, \tfrac{a+b}{2}, b\right),M(s,a,b)=M(ℓ,a,2a+b​)⌢(2a+b​)⌢M(r,2a+b​,b),

where ⌢\frown⌢ denotes concatenation of lists. The marks of ttt are then

marks⁡(t)=(0)⌢M(t,0,1)⌢(1).\operatorname{marks}(t) = (0) \frown M(t,0,1) \frown (1).marks(t)=(0)⌢M(t,0,1)⌢(1).

Concretely, if ttt has NNN leaves then marks⁡(t)\operatorname{marks}(t)marks(t) is a list of N+1N+1N+1 real numbers, strictly increasing, beginning with 000 and ending with 111; it lists the endpoints of the subdivision of [0,1][0,1][0,1] into NNN standard dyadic intervals obtained by repeatedly halving according to the shape of ttt. For example, the marks of a single leaf are (0,1)(0,1)(0,1); the marks of the node with two leaf subtrees are (0,12,1)(0,\tfrac12,1)(0,21​,1); the marks of the node whose left subtree is a leaf and whose right subtree is the node with two leaf subtrees are (0,12,34,1)\left(0,\tfrac12,\tfrac34,1\right)(0,21​,43​,1); and the marks of the node whose left subtree is the node with two leaf subtrees and whose right subtree is a leaf are (0,14,12,1)\left(0,\tfrac14,\tfrac12,1\right)(0,41​,21​,1).

A tree diagram is a triple consisting of a tree t−t_-t−​ (the domain tree), a tree t+t_+t+​ (the range tree), and a guarantee that t−t_-t−​ and t+t_+t+​ have the same leaf count. In ordinary mathematical language: an ordered pair of trees with equally many leaves. Nothing else is required of the pair, and no bound is placed on the size of the trees.

Carets and reducedness

A node both of whose subtrees are single leaves will be called a caret. For a tree ttt and a natural number kkk, say that ttt has a caret at position kkk when the kkk-th and (k+1)(k+1)(k+1)-st leaves of ttt, counted from 000 in left-to-right order, are exactly the two leaves hanging from one such node. The underlying recursion is: a single leaf has a caret at no position; and for a node with left subtree ℓ\ellℓ of leaf count LLL and right subtree rrr,

  • if k+1<Lk+1 < Lk+1<L, the node has a caret at kkk exactly when ℓ\ellℓ does;
  • if L≤kL \le kL≤k, the node has a caret at kkk exactly when rrr has a caret at position k−Lk - Lk−L;
  • in the remaining case k=L−1k = L-1k=L−1 (the two leaves straddle the root), the node has a caret at kkk exactly when ℓ\ellℓ and rrr are both single leaves.

In particular, if ttt has NNN leaves then ttt has a caret at no position k≥N−1k \ge N-1k≥N−1: for such kkk the recursion runs off the right-hand end of the tree and returns "no". For instance, the three-leaf tree with a leaf on the left and a caret on the right has a caret at position 111 and nowhere else, while the three-leaf tree with a caret on the left and a leaf on the right has a caret at position 000 and nowhere else.

A tree diagram (t−,t+)(t_-,t_+)(t−​,t+​) is reduced when

for every natural number k:not both t− and t+ have a caret at position k.\text{for every natural number } k: \quad \text{not both } t_- \text{ and } t_+ \text{ have a caret at position } k .for every natural number k:not both t−​ and t+​ have a caret at position k.

Because the quantifier runs over all natural numbers while a caret can only occur at a position below N−1N-1N−1 (where NNN is the common leaf count), this is a genuine restriction only for 0≤k≤N−20 \le k \le N-20≤k≤N−2; for every larger kkk both conjuncts are false and the condition holds automatically. If either tree is a single leaf, the condition holds vacuously.

What it is for a diagram to represent a map

A tree diagram (t−,t+)(t_-,t_+)(t−​,t+​) represents f∈Gf \in Gf∈G when all three of the following hold. Write marks⁡(t−)=(u0,u1,…,uN)\operatorname{marks}(t_-) = (u_0,u_1,\dots,u_N)marks(t−​)=(u0​,u1​,…,uN​) and marks⁡(t+)=(v0,v1,…,vN)\operatorname{marks}(t_+) = (v_0,v_1,\dots,v_N)marks(t+​)=(v0​,v1​,…,vN​), which have the same length N+1N+1N+1 because the two trees have the same leaf count NNN.

  1. f∈Ff \in Ff∈F, in the sense of the subgroup generated by the maps with property TTT described above.

  2. Affineness along the marks of the domain tree. For each index iii with 0≤i≤N−10 \le i \le N-10≤i≤N−1 there exist real numbers aia_iai​ and cic_ici​ such that

f^(z)=aiz+cifor all z with ui≤z≤ui+1.\hat f(z) = a_i z + c_i \qquad \text{for all } z \text{ with } u_i \le z \le u_{i+1}.f^​(z)=ai​z+ci​for all z with ui​≤z≤ui+1​.

The slopes aia_iai​ here are arbitrary real numbers: they are not required to be powers of two, nor positive, nor non-zero. The condition is imposed on consecutive pairs of the marks of the domain tree only; no affineness condition is imposed along the marks of the range tree. Since [ui,ui+1]⊆[0,1][u_i,u_{i+1}] \subseteq [0,1][ui​,ui+1​]⊆[0,1], on these intervals f^\hat ff^​ is just fff.

  1. The marks are carried over in order. Applying f^\hat ff^​ to each entry of marks⁡(t−)\operatorname{marks}(t_-)marks(t−​) yields exactly the list marks⁡(t+)\operatorname{marks}(t_+)marks(t+​):
(f^(u0),f^(u1),…,f^(uN))=(v0,v1,…,vN),\big(\hat f(u_0), \hat f(u_1), \dots, \hat f(u_N)\big) = (v_0,v_1,\dots,v_N),(f^​(u0​),f^​(u1​),…,f^​(uN​))=(v0​,v1​,…,vN​),

that is, f(ui)=vif(u_i) = v_if(ui​)=vi​ for every iii. This is an equality of lists, so it includes the assertion that the two lists have the same length; that part is automatic from the equality of leaf counts.

The statement being asserted

For every order-automorphism fff of the unit interval [0,1][0,1][0,1] which belongs to FFF — the subgroup of the group of order-automorphisms of [0,1][0,1][0,1] generated by all maps having property TTT (piecewise affine with slopes integral powers of two, with finitely many breakpoints, all dyadic) — there exists a tree diagram (t−,t+)(t_-,t_+)(t−​,t+​), i.e. a pair of finite binary trees with the same number NNN of leaves, such that:

  • the diagram is reduced: there is no position kkk at which t−t_-t−​ and t+t_+t+​ both have a caret whose two children are leaves; and
  • the diagram represents fff: fff lies in FFF; the extension of fff by the identity outside [0,1][0,1][0,1] is affine (with some real slope and intercept, possibly different on each piece) on each of the NNN closed intervals cut out by consecutive marks of t−t_-t−​; and fff carries the N+1N+1N+1 marks of t−t_-t−​, in order, onto the N+1N+1N+1 marks of t+t_+t+​.

The quantifier over fff is universal; fff is an ordinary variable of the statement (it is supplied implicitly rather than written out at each use, which does not change the assertion). The quantifier over diagrams is a bare existential: existence of such a diagram is claimed, not uniqueness, and no bound on NNN is claimed. There are no side conditions of any other kind: no typeclass or structural hypotheses beyond those already contained in "fff is an order-automorphism of [0,1][0,1][0,1]" and "f∈Ff \in Ff∈F".

Note that the first clause of "represents" repeats the hypothesis verbatim, so it adds nothing to what must be produced.

Degenerate and edge cases

  • The hypothesis is satisfiable, and by more than one map. FFF is a subgroup, so the identity map of [0,1][0,1][0,1] lies in FFF. It also contains non-identity maps: the map
z↦{z/2,0≤z≤1/2,z−1/4,1/2≤z≤3/4,2z−1,3/4≤z≤1,z \mapsto \begin{cases} z/2, & 0 \le z \le 1/2,\\ z - 1/4, & 1/2 \le z \le 3/4,\\ 2z-1, & 3/4 \le z \le 1,\end{cases}z↦⎩⎨⎧​z/2,z−1/4,2z−1,​0≤z≤1/2,1/2≤z≤3/4,3/4≤z≤1,​

has property TTT, taking B={1/2,3/4}B = \{1/2, 3/4\}B={1/2,3/4} (both dyadic), and hence lies in FFF; it is not the identity, since it sends 1/21/21/2 to 1/41/41/4. So the statement is not vacuous.

  • The conclusion can be met. For the identity map, the diagram in which both trees are a single leaf works: it is reduced (a single leaf has no carets), its domain marks are (0,1)(0,1)(0,1), the identity is affine on [0,1][0,1][0,1] with slope 111 and intercept 000, and the image of (0,1)(0,1)(0,1) is (0,1)(0,1)(0,1), the marks of the range tree. For the non-identity map displayed above, the diagram whose domain tree has marks (0,12,34,1)\left(0,\tfrac12,\tfrac34,1\right)(0,21​,43​,1) (a node with a leaf on the left and a caret on the right) and whose range tree has marks (0,14,12,1)\left(0,\tfrac14,\tfrac12,1\right)(0,41​,21​,1) (a node with a caret on the left and a leaf on the right) works: the two trees have three leaves each, their caret positions are 111 and 000 respectively, so no position carries a caret in both, and the map is affine on each of [0,12][0,\tfrac12][0,21​], [12,34][\tfrac12,\tfrac34][21​,43​], [34,1][\tfrac34,1][43​,1] and sends 0,12,34,10,\tfrac12,\tfrac34,10,21​,43​,1 to 0,14,12,10,\tfrac14,\tfrac12,10,41​,21​,1. So the conclusion is satisfiable, and not only by the one-leaf diagram.

  • The one-leaf diagram is not a universal witness. If both trees of a diagram are a single leaf, the reducedness condition is automatic, but the representation conditions say exactly that f^\hat ff^​ is affine on all of [0,1][0,1][0,1] and sends (0,1)(0,1)(0,1) to (0,1)(0,1)(0,1); combined with f(0)=0f(0)=0f(0)=0 and f(1)=1f(1)=1f(1)=1 this forces fff to be the identity. For any other fff in FFF the existential must be witnessed by a larger diagram.

  • Reducedness beyond the last leaf. As noted, the condition is quantified over all natural numbers kkk including those exceeding the number of leaves; at those positions neither tree has a caret, so nothing is asserted there. Reducedness is exactly the finitely many conditions at positions 0,…,N−20,\dots,N-20,…,N−2.

  • No dyadic or power-of-two condition appears in the conclusion. The slopes in the affineness clause are unconstrained reals, and there is no separate requirement that the marks form a standard dyadic partition — though they do so automatically, by the construction of marks from a tree.

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