Read-back: what the statement asserts

The declaration is a single implication with two universally quantified (implicitly bound) variables, three named hypotheses, and an existential conclusion. Everything it mentions is built up from the definitions unfolded below, so the whole assertion is restated here without reference to any other document.

The ambient group

Write $I = [0,1] \subseteq \mathbb{R}$, regarded as an ordered set with the order inherited from $\mathbb{R}$ (formally, the set of real numbers $x$ with $0 \le x$ and $x \le 1$, made into a type).

Let

$$G \;=\; \{\, f : I \to I \;:\; f \text{ is a bijection and } x \le y \iff f(x) \le f(y) \,\}$$

be the set of order isomorphisms of $I$ onto itself. No continuity, piecewise linearity or differentiability is assumed of a member of $G$: only that it is an order-preserving bijection of $I$ onto $I$.

$G$ is a group under composition, with

• product: $(g \cdot h)(x) = g(h(x))$ — so in a product the right factor acts first;
• identity $1 = \mathrm{id}_I$;
• inverse $g^{-1}$ = the inverse bijection;
• $g^0 = 1$ and $g^{n+1} = g^{n}\cdot g$ for $n \in \mathbb{N}$, i.e. $g^n$ is the $n$-fold composite of $g$ with itself.

Two elements of $G$ are equal exactly when they agree at every point of $I$.

For $f \in G$, let $\widetilde f : \mathbb{R} \to \mathbb{R}$ be the map

$$\widetilde f(x) = \begin{cases} f(x), & 0 \le x \le 1,\\ x, & \text{otherwise,}\end{cases}$$

i.e. $f$ extended to the whole line by the identity; this $\widetilde f$ is an order isomorphism of $\mathbb{R}$.

Dyadic numbers, "Thompson" elements, and the subgroup $F$

A real number $x$ is dyadic if $x = m/2^{k}$ for some $m \in \mathbb{Z}$ and $k \in \mathbb{N}$. (No restriction to $[0,1]$.)

Call $g \in G$ a Thompson element if there is a finite set $B \subseteq \mathbb{R}$, all of whose members are dyadic, such that:

for all $x, y \in I$ with $x < y$ and $(x,y) \cap B = \varnothing$ (open interval), there exist an integer $n$ and a real number $c$ such that

$$g(z) = 2^{n} z + c \qquad \text{for every } z \in I \text{ with } x \le z \le y .$$

Here $2^n$ is an integer power of $2$ (so a positive real), while $c$ is an arbitrary real number. $B$ is not required to be contained in $[0,1]$, nor to be non-empty.

Let $F \le G$ be the subgroup generated by the set of all Thompson elements: the intersection of all subgroups of $G$ containing that set, equivalently the set of all finite products of Thompson elements and inverses of Thompson elements (together with the identity). The hypothesis below asks only that $f$ lie in $F$; it does not ask that $f$ itself be a Thompson element.

The two distinguished elements $A$ and $B$

$A \in G$ is the map

$$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 continuous, piecewise-linear, increasing bijection of $I$: the three overlapping clauses agree at $x = \tfrac12$ and $x = \tfrac34$, and $A(0)=0$, $A(1)=1$).

$B \in G$ is the map

$$B(x) = \begin{cases} x, & 0 \le x \le \tfrac12,\\[2pt] \tfrac{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}$$

again continuous, piecewise linear and increasing, fixing $0$ and $1$ and fixing every point of $[0,\tfrac12]$.

(Both are defined as the restriction to $I$ of an explicit increasing piecewise-linear bijection of $\mathbb{R}$ that is the identity outside $[0,1]$.)

The elements $X_i$ and the words

Define $X_i \in G$ for $i \in \mathbb{N}$ by

$$X_0 = A, \qquad X_{n+1} = (A^{n})^{-1} \cdot B \cdot A^{n} \quad (n \in \mathbb{N}).$$

Note the index shift: the conjugating power is $n$, not $n+1$. Thus

$$X_1 = B, \quad X_2 = A^{-1} B A, \quad X_3 = A^{-2} B A^{2}, \quad\dots,\quad X_k = A^{-(k-1)} B A^{k-1} \ (k \ge 1),$$

which as a function means $X_k(x) = A^{-(k-1)}\bigl(B\bigl(A^{k-1}(x)\bigr)\bigr)$: the innermost (rightmost) factor acts first.

For a finite list $c = (c_0, c_1, \dots, c_{m-1})$ of natural numbers, define

$$w(c) \;=\; X_0^{\,c_0} \cdot X_1^{\,c_1} \cdots X_{m-1}^{\,c_{m-1}} \ \in G ,$$

the product taken in this left-to-right order, with $w(\text{empty list}) = 1$. The $k$-th entry of the list is the exponent of $X_k$: the list position determines which generator, starting at index $0$ and increasing by one along the list. Because the entries are natural numbers, all exponents occurring in $w(c)$ are $\ge 0$; entries equal to $0$ contribute the identity factor.

Consequently

$$w(c)^{-1} = X_{m-1}^{-c_{m-1}} \cdots X_1^{-c_1} X_0^{-c_0},$$

the inverted factors appearing in decreasing index order.

Trees, leaf counts, subdivision points, and exposed carets

A tree here is a finite rooted binary tree in which every node is either a leaf or has an ordered pair of subtrees (left, right). Its leaf count is $1$ for a leaf and the sum of the leaf counts of the two subtrees otherwise.

Subdivision points. Give the root the interval $[0,1]$; if a node carries $[a,b]$, its left subtree carries $[a,\frac{a+b}2]$ and its right subtree carries $[\frac{a+b}2, b]$. The marks of a tree $t$ is the list

$$\mathrm{marks}(t) \;=\; \bigl(0,\; \text{midpoints of the internal nodes in left-to-right (in-order) traversal},\; 1\bigr).$$

If $t$ has $n$ leaves, this list has $n+1$ entries and is strictly increasing,

$$\mathrm{marks}(t) = (x_0, x_1, \dots, x_n), \qquad 0 = x_0 < x_1 < \cdots < x_n = 1,$$

and $[x_{i-1}, x_i]$ is exactly the interval carried by the $i$-th leaf from the left. For the one-leaf tree, $\mathrm{marks} = (0,1)$. All these points are dyadic.

Exposed carets. For a tree $t$ and $k \in \mathbb{N}$, say $t$ has an exposed caret at $k$ when $t$ contains a node both of whose subtrees are single leaves, and the left of those two leaves is the $k$-th leaf of $t$ counted from the left starting at $0$. (The recursion implementing this descends into the left subtree when $k+1$ is less than its leaf count, into the right subtree with $k$ reduced by the left leaf count when $k$ is at least that leaf count, and in the one remaining case — $k$ = (left leaf count) $-1$, i.e. $k$ and $k+1$ straddle the node — returns true exactly when both subtrees are single leaves.) In particular a one-leaf tree has an exposed caret at no $k$, and no tree has an exposed caret at any $k$ beyond its leaf count.

Tree diagrams, representation, reducedness

A tree diagram $d$ consists of two trees, $\mathrm{dom}(d)$ and $\mathrm{ran}(d)$, together with (as part of the data) the requirement that they have the same leaf count. Write $\mathrm{marks}(\mathrm{dom}(d)) = (x_0,\dots,x_n)$ and $\mathrm{marks}(\mathrm{ran}(d)) = (y_0,\dots,y_n)$; these two lists have the same length $n+1$ precisely because of that requirement.

Say $d$ represents $f \in G$ when all three of the following hold.

1. $f \in F$ (the subgroup described above).
2. Affine on the pieces: for each pair of consecutive entries $x_{i}, x_{i+1}$ of $\mathrm{marks}(\mathrm{dom}(d))$ (so $i = 0, \dots, n-1$) there exist real numbers $a$ and $c$ with

$$\widetilde f(z) = a z + c \qquad \text{for all } z \text{ with } x_i \le z \le x_{i+1}.$$

Since $0 \le x_i < x_{i+1} \le 1$, this says $f(z) = az+c$ on $[x_i, x_{i+1}] \subseteq I$. Nothing requires $a > 0$, nor that $a$ be a power of $2$, nor that $c$ be dyadic; the slope and intercept may depend on $i$. 3. Marks go to marks, in order: applying $\widetilde f$ entrywise to the list $\mathrm{marks}(\mathrm{dom}(d))$ yields the list $\mathrm{marks}(\mathrm{ran}(d))$:

$$f(x_i) = y_i \qquad \text{for every } i = 0, 1, \dots, n.$$

(Equality of lists, so entry by entry and in the same order, not merely equality of the underlying sets.)

Say $d$ is reduced when there is no $k \in \mathbb{N}$ such that $\mathrm{dom}(d)$ has an exposed caret at $k$ and $\mathrm{ran}(d)$ has an exposed caret at $k$ — the same index $k$ in both trees. The quantifier runs over all natural numbers $k$, including those exceeding the leaf count, where both conditions fail anyway. A diagram whose two trees are both the one-leaf tree is reduced.

The condition on the pair of exponent lists

For two lists $a = (a_0, \dots, a_{m-1})$ and $b = (b_0, \dots, b_{m'-1})$ of natural numbers, say the pair $(a,b)$ — in this order — is normal-form data when all four of the following hold.

1. $a$ is not the empty list, i.e. $m \ge 1$.
2. The lists have equal length: $m = m'$.
3. At the last index $m-1$, exactly one of the two final entries vanishes and the other is strictly positive:

$$\bigl(a_{m-1} = 0 \ \text{and}\ b_{m-1} > 0\bigr) \quad\text{or}\quad \bigl(a_{m-1} > 0 \ \text{and}\ b_{m-1} = 0\bigr).$$

(This is a disjunction of two mutually exclusive alternatives; it rules out both $a_{m-1} = b_{m-1} = 0$ and $a_{m-1}, b_{m-1}$ both positive.) 4. For every $k \in \mathbb{N}$ with $k + 1 < m$:

$$\text{if } a_k > 0 \text{ and } b_k > 0, \text{ then } a_{k+1} > 0 \text{ or } b_{k+1} > 0 .$$

This is vacuous when $m = 1$. It is an implication in one direction only: nothing is claimed when $a_k = 0$ or $b_k = 0$, and the conclusion is an inclusive "or".

In clauses 3 and 4 the index bounds are computed from the length of the first list, which by clause 2 is also the length of the second, so every entry referred to genuinely exists. (Entries are read by a total lookup that returns $0$ for an out-of-range index; clauses 2–4 never rely on that, although clause 1 is what stops clause 3 from reading two out-of-range $0$'s when $a$ is empty — with $a$ empty, clause 3 would read $a_{\,\cdot} = b_{\,\cdot} = 0$ and fail.)

The assertion

Let $d$ be any tree diagram and let $f$ be any order isomorphism of $[0,1]$ onto itself (both universally quantified; in the Lean text they are implicit arguments, to be inferred, which does not change the logical content). Assume:

• (i) $d$ is reduced, in the sense above;
• (ii) $d$ represents $f$, in the three-part sense above (in particular $f \in F$);
• (iii) $f \ne 1$, i.e. $f$ is not the identity map of $[0,1]$.

Then there exist two finite lists $a = (a_0,\dots,a_{m-1})$ and $b = (b_0,\dots,b_{m-1})$ of natural numbers such that the pair $(a,b)$ is normal-form data (clauses 1–4) and

$$f \;=\; w(b) \cdot w(a)^{-1},$$

that is,

$$f \;=\; X_0^{\,b_0} X_1^{\,b_1} \cdots X_{m-1}^{\,b_{m-1}}\, > X_{m-1}^{-a_{m-1}} \cdots X_1^{-a_1} X_0^{-a_0},$$

an equality in $G$ (equivalently: the two sides agree at every point of $[0,1]$).

Points of the conclusion worth stating explicitly:

• The second list $b$ supplies the un-inverted (leftmost) block of factors and the first list $a$ supplies the inverted block, even though the normal-form-data condition is applied to the pair in the order $(a,b)$. So in the equation the roles are: $b$ positive, $a$ negative.
• In the inverted block the factors occur in decreasing generator index, while in the positive block they occur in increasing generator index.
• All $a_k, b_k$ are natural numbers, hence $\ge 0$; interior entries may be $0$.
• This is a plain existence claim ($\exists$, not $\exists!$): no uniqueness of $a$, $b$ or of $m$ is asserted, no minimality of $m$, and no bound on $m$ in terms of $d$ or $f$ (in particular no relation between $m$ and the number of leaves of the trees of $d$).
• Nothing is asserted about how $a$ and $b$ are obtained from $d$; the trees of $d$ do not appear in the conclusion.

Degenerate and edge cases the quantifiers include

• The hypotheses are jointly satisfiable, so the statement is not vacuous. An explicit witness: take $f = A$, $\mathrm{dom}(d)$ the tree whose left subtree is a leaf and whose right subtree is a caret of two leaves (marks $(0, \tfrac12, \tfrac34, 1)$), and $\mathrm{ran}(d)$ the tree whose left subtree is a caret of two leaves and whose right subtree is a leaf (marks $(0, \tfrac14, \tfrac12, 1)$). Both have $3$ leaves; $A$ carries $(0,\tfrac12,\tfrac34,1)$ to $(0,\tfrac14,\tfrac12,1)$ entrywise and is affine on each of the three pieces; $A$ is a Thompson element (breakpoint set $\{0,\tfrac12,\tfrac34,1\}$, slopes $2^{-1}, 2^{0}, 2^{1}$), hence lies in $F$; the domain tree has an exposed caret only at $k=1$ and the range tree only at $k=0$, so the diagram is reduced; and $A \ne 1$ since $A(\tfrac12) = \tfrac14$. (This witness was checked mechanically.)
• One-leaf diagrams cannot satisfy the hypotheses. If both trees of $d$ are single leaves then $\mathrm{marks} = (0,1)$ for each, and clause 2 of "represents" forces $f$ to be affine on all of $[0,1]$ while clause 3 forces $f(0)=0$, $f(1)=1$; hence $f = \mathrm{id}$, excluded by hypothesis (iii). So hypothesis (iii) is doing work beyond mere non-triviality of bookkeeping.
• The condition "$d$ is reduced" is a statement about matching indices: a diagram in which both trees have exposed carets, but never at the same index $k$, is reduced.
• The condition "affine on the pieces" is imposed only on the pieces cut out by the marks of the domain tree; no separate condition is imposed on the pieces of the range tree.
• Hypothesis (ii) requires $f \in F$ as a separate conjunct; it is not derived from the other two conjuncts inside this statement.
• There is no hypothesis that $f$ be continuous, piecewise linear, or have dyadic breakpoints beyond what (ii) provides, and no typeclass or finiteness hypothesis beyond those listed.