Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

FFF is generated by AAA and BBB

Proved
CannonFloydParry.closure_mapA_mapB_eq_F

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

dynamical-systemsgroup-theorypiecewise-linearthompsons-group

Thompson's group FFF is generated, as a subgroup of the group of order isomorphisms of [0,1][0,1][0,1], by the two elements AAA and BBB of Example 1.1, where

A(x)=x2 (0≤x≤12),x−14 (12≤x≤34),2x−1 (34≤x≤1)A(x) = \tfrac{x}{2}\ (0 \le x \le \tfrac12), \quad x - \tfrac14\ (\tfrac12 \le x \le \tfrac34), \quad 2x-1\ (\tfrac34 \le x \le 1)A(x)=2x​ (0≤x≤21​),x−41​ (21​≤x≤43​),2x−1 (43​≤x≤1)

and

B(x)=x (0≤x≤12),x2+14 (12≤x≤34),x−18 (34≤x≤78),2x−1 (78≤x≤1).B(x) = x\ (0 \le x \le \tfrac12), \quad \tfrac{x}{2}+\tfrac14\ (\tfrac12 \le x \le \tfrac34), \quad x - \tfrac18\ (\tfrac34 \le x \le \tfrac78), \quad 2x-1\ (\tfrac78 \le x \le 1).B(x)=x (0≤x≤21​),2x​+41​ (21​≤x≤43​),x−81​ (43​≤x≤87​),2x−1 (87​≤x≤1).

The source obtains this from the tree-diagram normal form of section 2; the statement itself refers to no trees.

Formal statement
import Definitions.Def_CannonFloydParry
import Mathlib

namespace CannonFloydParry

theorem closure_mapA_mapB_eq_F : Subgroup.closure {mapA, mapB} = 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, Corollary 2.6, p. 224
Read-back

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

Read-back: what the statement asserts

0. The assertion in one sentence

Inside the group GGG of all order isomorphisms of the closed unit interval [0,1][0,1][0,1], the subgroup generated by a certain explicit two-element set {A,B}\{A,B\}{A,B} of such isomorphisms is equal to the subgroup generated by the set of all order isomorphisms of [0,1][0,1][0,1] satisfying an explicit "piecewise-affine with dyadic breakpoints and power-of-two slopes" condition.

It is a closed statement: it has no universally or existentially quantified variables of its own, no hypotheses, no explicit or implicit arguments, and no typeclass assumptions beyond those already baked into the fixed objects it names. Everything below is the unfolding of those fixed objects.

Sections 1–4 expand every ingredient; section 5 states the assertion; section 6 collects the degenerate and edge cases that the definitions silently admit.


1. The ambient group GGG

Write

I  =  [0,1]  =  {t∈R  :  0≤t≤1},I \;=\; [0,1] \;=\; \{t \in \mathbb{R} \;:\; 0 \le t \le 1\},I=[0,1]={t∈R:0≤t≤1},

regarded as a set of real numbers and ordered by the order it inherits from R\mathbb{R}R: for a,b∈Ia, b \in Ia,b∈I, a≤ba \le ba≤b means exactly a≤ba \le ba≤b as real numbers.

An order isomorphism of III is a bijection f:I→If : I \to If:I→I such that for all a,b∈Ia, b \in Ia,b∈I

a≤b⟺f(a)≤f(b).a \le b \quad\Longleftrightarrow\quad f(a) \le f(b).a≤b⟺f(a)≤f(b).

Equivalently: an increasing bijection of [0,1][0,1][0,1] onto itself. Note carefully what is not required: no continuity, no differentiability, no measurability, no piecewise structure. The ambient object is a purely order-theoretic one; the order-isomorphism condition is an "if and only if", i.e. it says fff reflects as well as preserves ≤\le≤, which for a bijection is the same as saying fff and f−1f^{-1}f−1 are both increasing.

GGG denotes the set of all order isomorphisms of III, made into a group by

  • multiplication == = composition, in the order (fg)(x)=f(g(x))(fg)(x) = f\bigl(g(x)\bigr)(fg)(x)=f(g(x)) — the right-hand factor is applied first;
  • identity element === the identity map of III;
  • inverse === the inverse function.

Two facts about GGG that follow from the definitions alone and are used silently throughout: every f∈Gf \in Gf∈G satisfies f(0)=0f(0) = 0f(0)=0 and f(1)=1f(1) = 1f(1)=1 (an increasing bijection of [0,1][0,1][0,1] must fix the least and greatest elements), and GGG is not required to consist of piecewise-linear maps — it is the full order-automorphism group of the interval.


2. The two distinguished elements AAA and BBB

Both are specific, fully explicit elements of GGG. Each is obtained by writing down an increasing bijection of the whole real line that is the identity outside [0,1][0,1][0,1], and then restricting it to [0,1][0,1][0,1]; the restriction is legitimate because each of those maps fixes every point of (−∞,0](-\infty,0](−∞,0] and every point of [1,∞)[1,\infty)[1,∞), and in particular fixes 000 and 111. The resulting elements of GGG are given on [0,1][0,1][0,1] by the following formulas.

The map AAA.

A(x)  =  {12x,0≤x≤12,x−14,12≤x≤34,2x−1,34≤x≤1.A(x) \;=\; \begin{cases} \tfrac{1}{2}x, & 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)=⎩⎨⎧​21​x,x−41​,2x−1,​0≤x≤21​,21​≤x≤43​,43​≤x≤1.​

The three formulas agree at the overlaps (A(12)=14A(\tfrac12) = \tfrac14A(21​)=41​, A(34)=12A(\tfrac34) = \tfrac12A(43​)=21​), and A(0)=0A(0) = 0A(0)=0, A(1)=1A(1) = 1A(1)=1. So AAA is affine on each of [0,12][0,\tfrac12][0,21​], [12,34][\tfrac12,\tfrac34][21​,43​], [34,1][\tfrac34,1][43​,1], with slopes 2−1,20,212^{-1}, 2^{0}, 2^{1}2−1,20,21 respectively and breakpoints 12\tfrac1221​ and 34\tfrac3443​.

The map BBB.

B(x)  =  {x,0≤x≤12,12x+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] \tfrac{1}{2}x + \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,21​x+41​,x−81​,2x−1,​0≤x≤21​,21​≤x≤43​,43​≤x≤87​,87​≤x≤1.​

Again the formulas agree at the overlaps (B(12)=12B(\tfrac12) = \tfrac12B(21​)=21​, B(34)=58B(\tfrac34) = \tfrac58B(43​)=85​, B(78)=34B(\tfrac78) = \tfrac34B(87​)=43​), and B(0)=0B(0) = 0B(0)=0, B(1)=1B(1) = 1B(1)=1. So BBB is the identity on [0,12][0,\tfrac12][0,21​] and is affine on each of [12,34][\tfrac12,\tfrac34][21​,43​], [34,78][\tfrac34,\tfrac78][43​,87​], [78,1][\tfrac78,1][87​,1], with slopes 2−1,20,212^{-1}, 2^{0}, 2^{1}2−1,20,21 and breakpoints 12,34,78\tfrac12, \tfrac34, \tfrac7821​,43​,87​.

AAA and BBB are distinct elements of GGG (for instance A(14)=18A(\tfrac14) = \tfrac18A(41​)=81​ while B(14)=14B(\tfrac14) = \tfrac14B(41​)=41​), so {A,B}\{A,B\}{A,B} is a genuine two-element subset of GGG.


3. The dyadic-piecewise-affine condition TTT

Call a real number ttt dyadic if

∃ m∈Z, ∃ k∈Nwitht=m2k.\exists\, m \in \mathbb{Z},\ \exists\, k \in \mathbb{N} \quad\text{with}\quad t = \frac{m}{2^{k}} .∃m∈Z, ∃k∈Nwitht=2km​.

Here mmm ranges over all integers (positive, negative and zero) and kkk over the natural numbers including 000; so every integer is dyadic, as are 000 and all negative dyadic rationals. The power 2k2^k2k is the ordinary kkk-fold product of the real number 222.

For f∈Gf \in Gf∈G, say that fff satisfies condition TTT when:

there exists a finite set B⊆R\mathcal{B} \subseteq \mathbb{R}B⊆R such that

  1. every element of B\mathcal{B}B is dyadic, and
  2. for all x,y∈[0,1]x, y \in [0,1]x,y∈[0,1] with x<yx < yx<y and with
(x,y)∩B=∅(x,y) \cap \mathcal{B} = \varnothing(x,y)∩B=∅

(the open interval (x,y)(x,y)(x,y) containing no element of B\mathcal{B}B), there exist an integer n∈Zn \in \mathbb{Z}n∈Z and a real number c∈Rc \in \mathbb{R}c∈R such that

f(z)  =  2nz+cfor every z∈[x,y]f(z) \;=\; 2^{n} z + c \qquad\text{for every } z \in [x,y]f(z)=2nz+cfor every z∈[x,y]

(the closed interval [x,y][x,y][x,y]).

Points of detail that the phrasing fixes, and which change the meaning if altered:

  • The quantifier order is: B\mathcal{B}B first (one finite set works for all pairs), then x,yx,yx,y, then nnn and ccc. So nnn and ccc may depend on xxx and yyy, but B\mathcal{B}B may not.
  • The hypothesis on x,yx,yx,y concerns the open interval (x,y)(x,y)(x,y), while the affine formula is demanded on the closed interval [x,y][x,y][x,y]. Consequently the formula is pinned down at the endpoints xxx and yyy as well, even when those endpoints themselves lie in B\mathcal{B}B.
  • The exponent nnn is an arbitrary integer, so the admissible slopes are exactly the numbers …,14,12,1,2,4,…\ldots, \tfrac14, \tfrac12, 1, 2, 4, \ldots…,41​,21​,1,2,4,… — all integer powers of 222, every one of them strictly positive. Negative nnn is read as 2n=1/2−n2^{n} = 1/2^{-n}2n=1/2−n.
  • The additive constant ccc is an arbitrary real number. Nothing in the condition requires ccc to be dyadic, rational, or in any way constrained.
  • xxx and yyy are constrained to lie in [0,1][0,1][0,1]; zzz likewise ranges over the points of [0,1][0,1][0,1] lying in [x,y][x,y][x,y], which (since x,y∈[0,1]x,y \in [0,1]x,y∈[0,1]) is all of [x,y][x,y][x,y].
  • No relation between B\mathcal{B}B and the actual set of breakpoints of fff is asserted: B\mathcal{B}B is merely some finite dyadic set outside which fff is affine in the above sense. It need not be minimal, and it need not be contained in [0,1][0,1][0,1].

Condition TTT is a property of a single map, not of a set of maps; it is not asserted anywhere that the collection of maps satisfying TTT is closed under composition or under inverses.


4. The two subgroups

For a subset S⊆GS \subseteq GS⊆G, the subgroup generated by SSS is the smallest subgroup of GGG containing SSS — literally, the intersection of all subgroups of GGG that contain SSS. Equivalently, it is the set of all elements expressible as a finite product

g1ε1g2ε2⋯grεr,r≥0,gi∈S,εi∈{+1,−1},g_1^{\varepsilon_1} g_2^{\varepsilon_2} \cdots g_r^{\varepsilon_r}, \qquad r \ge 0,\quad g_i \in S,\quad \varepsilon_i \in \{+1,-1\},g1ε1​​g2ε2​​⋯grεr​​,r≥0,gi​∈S,εi​∈{+1,−1},

with the empty product (r=0r = 0r=0) equal to the identity. In particular the generated subgroup always contains the identity, whatever SSS is, and is generated by SSS as a set — no ordering, multiplicity or finiteness condition on SSS is involved.

The two subgroups in play are:

  • ⟨A,B⟩\langle A, B\rangle⟨A,B⟩, the subgroup of GGG generated by the two-element set {A,B}\{A,B\}{A,B} described in section 2;
  • F  =  ⟨ { f∈G:f satisfies condition T } ⟩F \;=\; \bigl\langle\, \{\,f \in G : f \text{ satisfies condition } T \,\}\,\bigr\rangleF=⟨{f∈G:f satisfies condition T}⟩, the subgroup of GGG generated by the (in general infinite) set of all elements of GGG satisfying condition TTT of section 3.

Note that FFF is defined as the subgroup generated by the TTT-maps, not as the set of TTT-maps.


5. What the declaration asserts

  ⟨A,B⟩  =  F  \boxed{\;\langle A, B\rangle \;=\; F\;}⟨A,B⟩=F​

as subgroups of GGG. Equality of subgroups here is equality of the underlying subsets of GGG: the assertion is the conjunction of the two inclusions, i.e. that for every order isomorphism f:[0,1]→[0,1]f : [0,1] \to [0,1]f:[0,1]→[0,1],

f is a finite product of A±1,B±1⟺f is a finite product of maps satisfying T and their inverses.f \text{ is a finite product of } A^{\pm 1}, B^{\pm 1} \qquad\Longleftrightarrow\qquad f \text{ is a finite product of maps satisfying } T \text{ and their inverses.}f is a finite product of A±1,B±1⟺f is a finite product of maps satisfying T and their inverses.

This is an equality (iff), not an inclusion in either direction.


6. Degenerate cases and things the quantifiers silently admit

  • No hypotheses at all. The declaration has no antecedent, so there is no question of a hypothesis being vacuous or impossible to satisfy; the statement is an unconditional equation between two specific subgroups.

  • The empty breakpoint set is allowed in condition TTT. If B=∅\mathcal{B} = \varnothingB=∅, clause (1) holds trivially and clause (2) applies to every pair x<yx < yx<y in [0,1][0,1][0,1]; taking x=0,y=1x=0,y=1x=0,y=1 it then demands a single formula f(z)=2nz+cf(z) = 2^n z + cf(z)=2nz+c valid on all of [0,1][0,1][0,1]. So the condition is satisfiable with B=∅\mathcal{B} = \varnothingB=∅ — the identity map does so, with n=0n = 0n=0, c=0c = 0c=0 — and the generating set of FFF is in particular non-empty.

  • B\mathcal{B}B may contain points outside [0,1][0,1][0,1]. The condition on B\mathcal{B}B is only that it be finite and consist of dyadic reals. Since x,yx,yx,y are confined to [0,1][0,1][0,1], only the points of B\mathcal{B}B lying in (0,1)(0,1)(0,1) can ever make the hypothesis (x,y)∩B=∅(x,y) \cap \mathcal{B} = \varnothing(x,y)∩B=∅ fail.

  • B\mathcal{B}B need not be a subset of the moved set, nor related to fff at all beyond clause (2); e.g. adding extra dyadic points to a working B\mathcal{B}B never destroys condition TTT, since enlarging B\mathcal{B}B only weakens the hypothesis in clause (2).

  • Dyadicity of B\mathcal{B}B is required; dyadicity of the intercepts is not. Nothing in condition TTT says that the constants ccc, or the values f(z)f(z)f(z), are dyadic.

  • Slopes are integer powers of two, hence never zero or negative; but nnn is unbounded in both directions, so arbitrarily large and arbitrarily small slopes are permitted, and a single fff may use different nnn on different intervals.

  • Degenerate pairs x,yx,yx,y are excluded by x<yx < yx<y. The case x=yx = yx=y is not covered by clause (2), so no constraint is imposed by single points on their own.

  • Endpoint behaviour is automatic, not assumed. Every member of GGG fixes 000 and 111 because it is an increasing bijection of [0,1][0,1][0,1]; this is not listed as part of condition TTT, and condition TTT adds nothing about the endpoints beyond what clause (2) gives.

  • No topology anywhere. Neither GGG, nor condition TTT, nor AAA and BBB involve continuity as a hypothesis. (Affinity on closed subintervals as in clause (2) is the only regularity condition present, and it is a consequence of the clause rather than an assumption about fff.)

  • The set {A,B}\{A,B\}{A,B} is unordered and has exactly two elements (A≠BA \neq BA=B), so the left-hand side is the subgroup generated by these two maps together with their inverses; no claim is made about either map individually.

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

  • Endorsed by dbenbenn · Sep 15, 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