Read-back of the statement

The declaration is a single assertion with one explicit universally quantified variable, a "tree diagram", and no implicit arguments, no typeclass hypotheses and no side conditions beyond what is built into that variable's type. Everything below is an unfolding of the notions it uses.

The ambient group

Write $I=[0,1]=\{x\in\mathbb{R}: 0\le x\le 1\}$, regarded as a linearly ordered set with the order inherited from $\mathbb{R}$.

By an increasing bijection of $I$ I mean a bijection $f:I\to I$ together with the property that

$$f(x)\le f(y)\iff x\le y\qquad\text{for all }x,y\in I .$$

(The datum carried is the bijection, its two-sided inverse, and that equivalence; the equivalence in particular makes $f$ strictly increasing, and since $f$ is an order-preserving bijection of a set with a least and a greatest element, $f(0)=0$ and $f(1)=1$.)

These maps form a group. The product is composition, in the order

$$(f\cdot g)(x)=f\bigl(g(x)\bigr),$$

the neutral element is the identity map of $I$, and the inverse of $f$ is the inverse bijection.

Dyadic numbers, and the maps called Thompson maps

A real number $x$ is dyadic if $x=m/2^{k}$ for some integer $m$ (of either sign) and some natural number $k$. Since $k=0$ is allowed, every integer is dyadic.

An increasing bijection $f$ of $I$ is a Thompson map if there exists 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$, there exist an integer $n$ and a real $c$ with

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

Three points of literal detail. The exponent $n$ ranges over all of $\mathbb{Z}$, so the slope is any integral power of $2$ and in particular is positive; negative $n$ gives slope $2^{n}=1/2^{-n}$. The disjointness is tested on the open interval $(x,y)$ while the affine formula is asserted on the closed interval $[x,y]$. And $B$ is not required to be contained in $I$, nor to be non-empty: the empty set is an admissible choice of $B$, in which case the requirement is that $f$ be given on all of $I$ by a single formula $z\mapsto 2^{n}z+c$.

The group $F$

$F$ denotes the subgroup of the group of increasing bijections of $I$ generated by the set of Thompson maps: the smallest subgroup containing every Thompson map, equivalently the intersection of all subgroups containing every Thompson map, equivalently the set of all finite products of Thompson maps and of inverses of Thompson maps (the empty product being the identity).

So "$f\in F$" is literally membership in the generated subgroup, which is a priori a weaker demand than "$f$ is itself a Thompson map".

Extension of a map of $I$ to a map of $\mathbb{R}$

For an increasing bijection $f$ of $I$, let $\tilde f:\mathbb{R}\to\mathbb{R}$ be

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

This is an increasing bijection of $\mathbb{R}$ (it is monotone, bijective, and satisfies $\tilde f(x)\le\tilde f(y)\iff x\le y$). On $I$ it agrees with $f$ by construction.

Finite binary trees, and their marks

A tree is a finite rooted binary tree in the following inductive sense: either a single leaf, or a node built from an ordered pair $(l,r)$ of trees. Its leaf count is $1$ for a leaf and the sum of the leaf counts of $l$ and $r$ for a node built from $(l,r)$.

For a tree $t$ and reals $a,b$ define a finite list $M(t;a,b)$ of reals by recursion on $t$:

$$M(\text{leaf};a,b)=[\,],\qquad M(\text{node}(l,r);a,b)=M\!\left(l;a,\tfrac{a+b}{2}\right)\frown\left[\tfrac{a+b}{2}\right]\frown M\!\left(r;\tfrac{a+b}{2},b\right),$$

where $\frown$ is concatenation of lists. The marks of $t$ are the list

$$\operatorname{marks}(t)=[0]\frown M(t;0,1)\frown[1].$$

Facts about this recursion, each checked mechanically: $\operatorname{marks}(t)$ has length equal to the leaf count of $t$ plus one; its first entry is $0$ and its last entry is $1$; and it is strictly increasing. Hence writing $n$ for the leaf count of $t$,

$$\operatorname{marks}(t)=\bigl[x_0,x_1,\dots,x_n\bigr],\qquad 0=x_0<x_1<\cdots<x_n=1,$$

and all entries lie in $I$. Concretely:

• a single leaf gives $[0,1]$;
• $\text{node}(\text{leaf},\text{leaf})$ gives $[0,\tfrac12,1]$;
• $\text{node}(\text{node}(\text{leaf},\text{leaf}),\text{leaf})$ gives $[0,\tfrac14,\tfrac12,1]$;
• $\text{node}(\text{leaf},\text{node}(\text{leaf},\text{leaf}))$ gives $[0,\tfrac12,\tfrac34,1]$;
• $\text{node}(\text{node}(\text{leaf},\text{node}(\text{leaf},\text{leaf})),\text{leaf})$ gives $[0,\tfrac14,\tfrac38,\tfrac12,1]$.

So the recursion halves the current interval at each node, recursing into the left half with the left subtree and into the right half with the right subtree, and the marks are the endpoints of the resulting subdivision of $[0,1]$ into consecutive intervals, one per leaf.

Tree diagrams

A tree diagram consists of three components: a tree, called its domain tree; a tree, called its range tree; and a proof that the two trees have the same leaf count. The third component is proof-valued, hence proof-irrelevant: two tree diagrams with the same pair of trees are equal, and a tree diagram is exactly an ordered pair of trees with equal leaf counts. It is not an extra assumption one is allowed to use or to dispense with: it is a constraint on which pairs of trees constitute a diagram.

This type is inhabited — for instance take both trees to be a single leaf — so the assertion below is not vacuous for lack of diagrams.

What it means for a map to represent a diagram

Given a tree diagram $d$ with domain tree $t_{\mathrm{dom}}$ and range tree $t_{\mathrm{ran}}$, and an increasing bijection $f$ of $I$, write

$$\operatorname{marks}(t_{\mathrm{dom}})=[x_0,\dots,x_n],\qquad \operatorname{marks}(t_{\mathrm{ran}})=[y_0,\dots,y_n]$$

(the two lists have the same length because the leaf counts agree). Then "$f$ represents $d$" is the conjunction of exactly three clauses.

(i) $f\in F$, in the sense of the previous section.

(ii) (piecewise affineness, on the subdivision cut out by the domain tree only) For each $i$ with $0\le i\le n-1$ there exist real numbers $a_i$ and $c_i$ such that

$$\tilde f(z)=a_i\,z+c_i\qquad\text{for every real }z\text{ with }x_i\le z\le x_{i+1}.$$

Literal details: the condition is imposed only on consecutive pairs of entries of $\operatorname{marks}(t_{\mathrm{dom}})$, and on the closed interval $[x_i,x_{i+1}]$, so adjacent pieces are required to give the same value at the shared mark (which is automatic, both sides being $\tilde f$ of that mark). The slope $a_i$ is an arbitrary real number: this clause does not demand that it be a power of $2$, nor that it be positive or non-zero — although positivity is in fact forced, since $\tilde f$ is a strictly increasing bijection and $x_i<x_{i+1}$. The clause is stated for the extension $\tilde f$, but since all the $x_i$ lie in $I$ it constrains $\tilde f$ only on $[0,1]$, where $\tilde f$ agrees with $f$. Nothing is asked about the subdivision cut out by the range tree.

(iii) (equality of lists) Applying $\tilde f$ to each entry of $\operatorname{marks}(t_{\mathrm{dom}})$, in order, yields the list $\operatorname{marks}(t_{\mathrm{ran}})$:

$$\bigl[\tilde f(x_0),\tilde f(x_1),\dots,\tilde f(x_n)\bigr]=[y_0,y_1,\dots,y_n],$$

i.e. $f(x_i)=y_i$ for every $i$, entry by entry and in the same order. Being an equality of lists, it also forces the two lists to have the same length — a consequence already guaranteed by the diagram's leaf-count component. Note that clauses (ii) and (iii) together make no assertion about the values of $f$ anywhere other than: affine on each domain piece (ii), and the prescribed values at the domain marks (iii).

The assertion

For every tree diagram $d$ there exists an increasing bijection $f$ of $[0,1]$ that represents $d$ — i.e. such that $f$ lies in the subgroup generated by the Thompson maps, $f$ is affine on each of the closed intervals cut out by consecutive marks of the domain tree, and $f$ carries the marks of the domain tree, in order, onto the marks of the range tree.

It is a plain existence claim: $\exists f$, not $\exists! f$, and no uniqueness, canonicity or further property of $f$ is asserted. It is quantified over all tree diagrams, with no further hypothesis on the pair of trees beyond equal leaf counts — in particular no minimality, no reducedness, and no non-degeneracy.

Degenerate and edge cases included by the quantifier

• Both trees a single leaf. Then both mark lists are $[0,1]$, clause (ii) is the single requirement that $f$ be given by one affine formula on the whole of $[0,1]$, and clause (iii) says $f(0)=0$, $f(1)=1$; so the only witness is the identity.

• The two trees equal. If the domain and range trees of $d$ coincide, the identity map of $I$ satisfies all three clauses: it belongs to $F$ (being the neutral element of a subgroup — and it is in any case a Thompson map, with $B=\varnothing$, slope $2^{0}$ and intercept $0$); its extension to $\mathbb{R}$ is the identity of $\mathbb{R}$, which is affine with slope $1$ and intercept $0$ on every interval; and it maps every mark to itself. Hence for every such diagram the assertion is satisfied by an explicit witness and carries no content. More generally, the same witness works whenever the two mark lists are equal as lists. (Both of these were checked mechanically.) The quantifier includes these diagrams alongside the ones with distinct trees.

• Diagrams with distinct trees of the same leaf count exist, so the quantifier does range over non-degenerate cases; for example the domain tree $\text{node}(\text{node}(\text{leaf},\text{leaf}),\text{leaf})$ with marks $[0,\tfrac14,\tfrac12,1]$ and the range tree $\text{node}(\text{leaf},\text{node}(\text{leaf},\text{leaf}))$ with marks $[0,\tfrac12,\tfrac34,1]$, both of leaf count $3$.

• No clause constrains $f$ off $[0,1]$, and no clause refers to the subdivision determined by the range tree; the range tree enters only through clause (iii), as the list of target values of the marks.