Read-back: nine declarations

Throughout, "list" means a finite ordered sequence, possibly empty, with repetitions allowed. Several accounts below need the same two background objects, and each account restates what it needs, so the accounts may be read in any order and none of them requires the others.

The unit interval as a type. One of the ambient types is the set

$$I=[0,1]=\{x\in\mathbb R : 0\le x \ \text{and}\ x\le 1\},$$

regarded as a type in its own right: an element of it is a pair consisting of a real number $x$ together with a proof that $0\le x\le 1$, and the associated real number $x$ is recovered by the first projection. Below, an element of this type is silently identified with the real number it carries. Note the interval is closed: both $0$ and $1$ belong to it.

Order isomorphisms. For an ordered set $S$, an order isomorphism of $S$ is a bijection $L\colon S\to S$ together with the property that for all $x,y\in S$,

$$L(x)\le L(y)\iff x\le y.$$

(The data is: a map, an inverse map, proofs that the two compose to the identity in both directions, and the displayed equivalence.) For $S=\mathbb R$ or $S=[0,1]$ this is the same thing as an increasing bijection of $S$ onto itself. The order isomorphisms of $S$ form a group in which

• the product $g\cdot h$ is the composite that applies $h$ first, i.e. $(g\cdot h)(z)=g(h(z))$;
• the identity element is the identity map;
• the inverse $g^{-1}$ is the inverse bijection;
• consequently $g^0$ is the identity and $g^{m+1}=g^m\cdot g$, so $g^m$ is the $m$-fold composite of $g$ with itself, and $g^{-m}$ denotes $(g^m)^{-1}$.

---

1. IsStandardDyadicInterval

This is a property of an ordered pair of real numbers $(x,y)$ — a two-place relation on $\mathbb R$, not a set and not a single interval. It asserts:

There exist natural numbers $a$ and $n$ (so $a\ge 0$ and $n\ge 0$) such that

$$a+1\le 2^{n},\qquad x=\frac{a}{2^{n}},\qquad y=\frac{a+1}{2^{n}}.$$

Three points of literal detail.

The same $a$ and $n$ serve both equations. The quantifier is a single $\exists a\,\exists n$ governing all three conjuncts, so $y-x=2^{-n}$ exactly, and $x$ and $y$ are consecutive multiples of $2^{-n}$.

Where the arithmetic happens. The inequality $a+1\le 2^{n}$ is an inequality between natural numbers: $a$, $1$, $2$ and $2^n$ are all natural there, and $2^n$ is the natural-number power. The two equations are equations between real numbers: $a$ is converted to a real, and $2^{n}$ is the real number $2$ raised to the natural-number power $n$. No truncated (natural-number) subtraction or division occurs anywhere.

What the hypothesis $a+1\le 2^n$ buys. It is equivalent to $a<2^{n}$, i.e. $a\in\{0,1,\dots,2^{n}-1\}$. It is satisfiable for every $n$ (take $a=0$), so the relation is not vacuous. Together with $a\ge 0$ it forces

$$0\le x<y\le 1 .$$

So the relation holds only for pairs lying inside $[0,1]$ with $x$ strictly less than $y$; but note that "$x<y$" is a consequence of the three displayed conjuncts and is not itself written down as a hypothesis.

Degenerate case. If $n=0$ then $a+1\le 1$ forces $a=0$, and the pair is $(0,1)$. For each $n\ge 1$ there are exactly $2^{n}$ admissible pairs, namely $\bigl(a2^{-n},(a+1)2^{-n}\bigr)$ for $0\le a\le 2^n-1$. The same pair of reals may be witnessed only by the reduced choice of $(a,n)$, but the statement demands merely that some witness exist.

---

2. IsStandardDyadicPartition

This is a property of a list of real numbers $\langle x_1,x_2,\dots,x_m\rangle$ (the list is finite; $m$ may be $0$). It is the conjunction of exactly three conditions:

1. The list is nonempty and its first entry is $0$. (Literally: the "first entry, if any" of the list is present and equal to $0$. For the empty list no first entry is present, so the condition fails.)
2. The list is nonempty and its last entry is $1$, in the same sense.
3. Every pair of consecutive entries, taken in list order, satisfies the relation of §1: for each $i$ with $1\le i\le m-1$, there are natural numbers $a_i,n_i$ with $a_i+1\le 2^{n_i}$, $x_i=a_i/2^{n_i}$ and $x_{i+1}=(a_i+1)/2^{n_i}$.

Condition 3 is the "chain" condition. It constrains only adjacent pairs $(x_i,x_{i+1})$ in the order in which they occur; it says nothing directly about non-adjacent pairs, and it holds automatically (with nothing to check) for a list of length $0$ or $1$.

Edge cases. Because of 1 and 2, the empty list is not a standard dyadic partition, and no one-entry list is either: a one-entry list $\langle x\rangle$ would need $x=0$ from 1 and $x=1$ from 2. Hence any list satisfying all three conditions has at least two entries. The shortest example is $\langle 0,1\rangle$, for which condition 3 requires only the single pair $(0,1)$, witnessed by $a=0,n=0$.

What the three conditions amount to. By §1 each adjacent pair is strictly increasing, so the list is strictly increasing; combined with first entry $0$ and last entry $1$ the entries are $0=x_1<x_2<\dots<x_m=1$ and the closed intervals $[x_i,x_{i+1}]$ are standard dyadic intervals covering $[0,1]$ with disjoint interiors. Nothing beyond the three conditions is asserted; in particular the exponents $n_i$ are not required to be equal to one another, nor is any compatibility between successive witnesses imposed beyond the shared endpoint $x_{i+1}$.

---

3. TreeDiagram

This declaration introduces a type (a kind of mathematical object), not a proposition. It depends on the following notion of tree.

Finite binary trees. A tree is built by the two rules: there is a tree called the leaf; and from any two trees $l$ and $r$ one forms a tree, the node with left subtree $l$ and right subtree $r$. Two trees are equal only if built by identical sequences of these rules; in particular the node built from $(l,r)$ is distinct from the node built from $(r,l)$ unless $l=r$, so the trees are ordered (planar) rooted binary trees in which every internal vertex has exactly two children. Equality of trees is decidable.

Leaf count. The number of leaves of a tree is defined recursively: the leaf has $1$ leaf, and the node with subtrees $l$ and $r$ has (number of leaves of $l$) $+$ (number of leaves of $r$) leaves. This is a natural number, and it is at least $1$ for every tree.

A tree diagram is a triple consisting of:

• a tree, called the domain tree;
• a tree, called the range tree;
• a proof that the two trees have the same number of leaves.

So the third component is not an extra piece of numerical data but a requirement: only pairs of trees with equal leaf counts give rise to a tree diagram, and each tree diagram remembers which tree is the domain one and which is the range one. The two trees are allowed to be equal, and the pair (leaf, leaf) is admissible (both have one leaf), so the type is nonempty. No other condition is imposed — in particular the two trees need not have the same shape, the same number of internal vertices, or the same height.

---

4. AffineOnPieces

This is a property of a pair: an order isomorphism $L$ of the whole real line, and a list of real numbers $\langle x_1,\dots,x_m\rangle$. It asserts exactly this chain condition:

For every pair of consecutive entries of the list, in list order — that is, for each $i$ with $1\le i\le m-1$, with $u=x_i$ and $v=x_{i+1}$ — there exist real numbers $a$ and $c$ such that

$$L(z)=a z+c\qquad\text{for every real } z \text{ with } u\le z\le v.$$

Details that the wording is chosen to preserve.

Which pairs. Only adjacent pairs, and only in the given order: the first coordinate is the earlier entry. Nothing is asserted about $x_i$ and $x_j$ for $j>i+1$, and nothing about the behaviour of $L$ outside $[\,x_1,x_m\,]$.

The interval is closed at both ends. The condition ranges over $z$ with $u\le z\le v$, so the endpoints $x_i$ and $x_{i+1}$ themselves are included; consecutive constraints therefore overlap at the shared endpoint.

The constants are local and unconstrained. The numbers $a$ and $c$ are chosen inside the quantifier, so they may differ from one adjacent pair to the next. Neither $a\neq 0$ nor $a>0$ is required by the statement, and $a$ is a real number (no restriction to powers of $2$, to rationals or to positive numbers appears). That $L$ is an increasing bijection forces $a>0$ whenever $u<v$; that is a consequence, not a hypothesis.

Degenerate cases. For a list with fewer than two entries — the empty list, or a one-entry list — there are no adjacent pairs and the condition holds for every $L$, with nothing to verify. If some adjacent pair has $x_i>x_{i+1}$, then the set of $z$ with $x_i\le z\le x_{i+1}$ is empty and the requirement for that pair is satisfied by any $a$ and $c$ whatsoever; the property does not itself demand that the list be increasing. Repeated entries $x_i=x_{i+1}$ likewise impose only the one-point condition $L(x_i)=ax_i+c$, which is always solvable.

---

5. Represents

This is a property of a pair: a tree diagram $d$ (as in §3) and an order isomorphism $f$ of the closed unit interval $[0,1]$. Four auxiliary notions enter, and all of them are spelled out below.

(a) The subdivision list of a tree. To a tree $t$ one attaches a finite list of real numbers as follows. First, for a tree $t$ and reals $a<b$ define a list $M(t;a,b)$ recursively:

• $M(\text{leaf};a,b)$ is the empty list;
• for the node with subtrees $l,r$, writing $m=\tfrac{a+b}{2}$,

$$M(\text{node}(l,r);a,b)\;=\;M(l;a,m)\ \frown\ \langle m\rangle\ \frown\ M(r;m,b),$$

the concatenation of the list for $l$ on $[a,m]$, then the single entry $m$, then the list for $r$ on $[m,b]$.

The list attached to $t$ is then

$$\mathrm{marks}(t)\;=\;\langle 0\rangle\ \frown\ M(t;0,1)\ \frown\ \langle 1\rangle .$$

Concretely this is the increasing list of all endpoints of the subdivision of $[0,1]$ obtained by repeatedly bisecting according to $t$: the root corresponds to $[0,1]$, and each node splits its interval at the midpoint, the left subtree taking the left half and the right subtree the right half. Its first entry is $0$, its last entry is $1$, and its length is (number of leaves of $t$) $+\,1$. For example the leaf gives $\langle 0,1\rangle$; the node with two leaves gives $\langle 0,\tfrac12,1\rangle$; the node whose left subtree is a node of two leaves and whose right subtree is a leaf gives $\langle 0,\tfrac14,\tfrac12,1\rangle$.

(b) Extension by the identity. Given an order isomorphism $f$ of $[0,1]$, let $\tilde f\colon \mathbb R\to\mathbb R$ be

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

This $\tilde f$ is an increasing bijection of $\mathbb R$, i.e. an order isomorphism of $\mathbb R$, and it agrees with $f$ on $[0,1]$ (including at the endpoints $0$ and $1$, which $f$ must fix since it is an increasing bijection of $[0,1]$).

(c) The ambient group. Call an order isomorphism $g$ of $[0,1]$ piecewise dyadic-affine if:

there exists a finite set $B$ of real numbers, each element $b$ of which is a dyadic rational in the sense that $b=m/2^{k}$ for some integer $m$ (possibly negative) and some natural number $k$, such that for all $x,y\in[0,1]$ with $x<y$ whose open interval $(x,y)$ meets $B$ not at all, there exist an integer $n$ and a real $c$ with

$$g(z)=2^{n}z+c \quad\text{for every } z\in[0,1] \text{ with } x\le z\le y .$$

Here $2^{n}$ is a real integer power of $2$, so the admissible slopes are $\dots,\tfrac14,\tfrac12,1,2,4,\dots$, always strictly positive; $n$ and $c$ may depend on $x$ and $y$; the interval on which the affine formula is required is the closed interval $[x,y]$, while the set that must avoid $B$ is the open interval $(x,y)$; the elements of $B$ are arbitrary dyadic rationals and are not required to lie in $[0,1]$; and $B$ is allowed to be empty, in which case $g$ must be $z\mapsto 2^{n}z+c$ on all of $[0,1]$.

Let $G$ be the smallest subgroup of the group of all order isomorphisms of $[0,1]$ that contains every piecewise dyadic-affine element — equivalently, the intersection of all subgroups containing them; equivalently again, the set of all finite products of piecewise dyadic-affine elements and their inverses, the empty product being the identity. Membership of $G$ is the first condition below. Note this is membership in the generated subgroup, which is weaker on its face than being itself piecewise dyadic-affine.

The assertion. "$d$ is represented by $f$" is the conjunction of exactly three statements:

1. $f\in G$;
2. $\tilde f$ is affine on the pieces cut out by the subdivision list of the domain tree of $d$: for each pair of consecutive entries $u,v$ of $\mathrm{marks}(d_{\mathrm{dom}})$ there are reals $a,c$ with $\tilde f(z)=az+c$ for all real $z$ with $u\le z\le v$ (the property of §4);
3. applying $\tilde f$ to every entry of $\mathrm{marks}(d_{\mathrm{dom}})$, entry by entry and keeping the order, yields exactly the list $\mathrm{marks}(d_{\mathrm{ran}})$ — equality of lists, hence equal lengths and equal entries in corresponding positions.

Remarks on what is and is not said. Condition 2 is imposed on the domain list only; no affineness condition is stated relative to the range list. Condition 3 is an equality of lists, not of sets, so the order is part of the claim; since the two trees of a tree diagram have the same number of leaves, the two lists have the same length automatically, and condition 3 is equivalent to the pointwise equalities $\tilde f(u_i)=v_i$ for all $i$, where $u_i$ and $v_i$ enumerate the domain and range subdivision lists. All the entries of these lists lie in $[0,1]$, so $\tilde f$ acts on them as $f$ does. Nothing here asserts that $f$ is determined by $d$, nor that every tree diagram is represented by something, nor that $f$ is piecewise dyadic-affine in the sense of (c).

---

6. X

This declaration defines, for every natural number $n$, an order isomorphism $X_n$ of the closed unit interval $[0,1]$. Two specific such isomorphisms are used, and both are described here.

The map $A$. $A$ is the restriction to $[0,1]$ of the increasing bijection of $\mathbb R$ given by

$$x\mapsto\begin{cases} x, & x\le 0,\\ x/2, & 0\le x\le \tfrac12,\\ x-\tfrac14, & \tfrac12\le x\le \tfrac34,\\ 2x-1, & \tfrac34\le x\le 1,\\ x, & 1\le x . \end{cases}$$

(The clauses agree on the overlaps, so the formula is unambiguous.) Thus $A$ is the piecewise linear increasing homeomorphism of $[0,1]$ with breakpoints at $0,\tfrac12,\tfrac34,1$, sending them to $0,\tfrac14,\tfrac12,1$ respectively, with slopes $\tfrac12,1,2$ on the three pieces.

The map $B$. $B$ is the restriction to $[0,1]$ of the increasing bijection of $\mathbb R$ given by

$$x\mapsto\begin{cases} x, & x\le\tfrac12,\\ \tfrac x2+\tfrac14, & \tfrac12\le x\le\tfrac34,\\ x-\tfrac18, & \tfrac34\le x\le\tfrac78,\\ 2x-1, & \tfrac78\le x\le 1,\\ x, & 1\le x . \end{cases}$$

Thus $B$ is the identity on $[0,\tfrac12]$, and on $[\tfrac12,1]$ it is the piecewise linear increasing homeomorphism with breakpoints $\tfrac12,\tfrac34,\tfrac78,1$ sent to $\tfrac12,\tfrac58,\tfrac34,1$, with slopes $\tfrac12,1,2$.

The definition. $X_n$ is given by cases on whether $n$ is zero or a successor:

$$X_0=A,\qquad\qquad X_{n+1}=\bigl(A^{\,n}\bigr)^{-1}\cdot B\cdot A^{\,n}\quad (n\ge 0),$$

the product being taken in the group of order isomorphisms of $[0,1]$ described at the top, and the two multiplications associating to the left: $\bigl((A^{n})^{-1}\cdot B\bigr)\cdot A^{n}$. Because that product applies its right factor first, as a map

$$X_{n+1}(z)=A^{-n}\bigl(B\bigl(A^{n}(z)\bigr)\bigr),$$

i.e. $X_{n+1}$ is the conjugate of $B$ that first pushes $z$ forward by $n$ applications of $A$, then applies $B$, then undoes the $n$ applications of $A$. The exponent $n$ here is the natural number appearing in the case split, so the exponents $A^{n}$ are nonnegative powers and $A^{-n}$ means the inverse of the $n$-fold composite.

Indexing. Because of the shift in the second clause, the index on the left is one more than the exponent on the right: $X_1$ involves $A^{0}$, $X_2$ involves $A^{1}$, and in general for $k\ge 1$ one has $X_k=A^{-(k-1)}BA^{\,k-1}$. In particular $X_1=B$ (see §8) and $X_2=A^{-1}BA$, meaning the map $z\mapsto A^{-1}(B(A(z)))$. The single index $0$ is the only one at which the first clause applies, so $X_0$ is $A$ and is not of the conjugate form.

---

7. X_zero

This asserts the single equality

$$X_0 = A$$

between elements of the group of order isomorphisms of the closed unit interval $[0,1]$, where $X_0$ is the value at $0$ of the family of §6 and $A$ is the piecewise linear increasing homeomorphism of $[0,1]$ described there, with breakpoints $0,\tfrac12,\tfrac34,1$ sent to $0,\tfrac14,\tfrac12,1$.

There are no quantifiers, no hypotheses and no free variables: it is a closed equation between two specific order isomorphisms of $[0,1]$. Equality here is equality of these objects, which for order isomorphisms is the same as equality of the underlying maps $[0,1]\to[0,1]$.

---

8. X_one

This asserts the single equality

$$X_1 = B$$

between elements of the group of order isomorphisms of $[0,1]$, where $X_1$ is the value at $1$ of the family of §6 and $B$ is the map described there: the identity on $[0,\tfrac12]$, and on $[\tfrac12,1]$ the piecewise linear increasing homeomorphism with breakpoints $\tfrac12,\tfrac34,\tfrac78,1$ sent to $\tfrac12,\tfrac58,\tfrac34,1$.

Again there are no quantifiers, hypotheses or free variables. Unwinding the definition of §6 at $n+1$ with $n=0$, the left-hand side is $\bigl(A^{0}\bigr)^{-1}\cdot B\cdot A^{0}$, i.e. the conjugate of $B$ by the empty power of $A$; the assertion is that this equals $B$.

---

9. IsPositive

This is a property of a single order isomorphism $f$ of the closed unit interval $[0,1]$. It asserts:

There exist a natural number $n$ and a function $b$ from the natural numbers to the natural numbers such that

$$f \;=\; X_0^{\,b(0)}\cdot X_1^{\,b(1)}\cdots X_n^{\,b(n)}\cdot 1,$$

where the $X_k$ are the order isomorphisms of §6, the product is taken in the group of order isomorphisms of $[0,1]$, the factors occur in increasing order of index from left to right, and the final factor is the identity element.

Precisely, the product is formed by folding the list of indices $\langle 0,1,2,\dots,n\rangle$ from the right onto the identity element: the result is

$$X_0^{\,b(0)}\cdot\Bigl(X_1^{\,b(1)}\cdot\bigl(\cdots\cdot\bigl(X_n^{\,b(n)}\cdot 1\bigr)\cdots\bigr)\Bigr),$$

so the factor of smallest index stands leftmost. Since the product of order isomorphisms applies its right factor first, as a map this means: apply $X_n^{\,b(n)}$ first, then $X_{n-1}^{\,b(n-1)}$, and finally $X_0^{\,b(0)}$.

Points of literal detail.

The exponents are natural numbers. $b$ takes values in $\mathbb N$, so every exponent $b(k)$ is $\ge 0$; no negative exponent may occur. ($g^{0}$ is the identity and $g^{m+1}=g^{m}\cdot g$.)

The list of indices always starts at $0$ and is nonempty. The index list is $\langle 0,1,\dots,n\rangle$, of length $n+1$; even the smallest choice $n=0$ gives the one-entry list $\langle 0\rangle$. So $X_0$ always appears as a factor, though possibly with exponent $0$. There is no choice of $n$ producing an empty product and no way to skip an index — an index is "skipped" only in the sense that its exponent may be $0$.

The function $b$ is total but only finitely much of it matters. $b$ is a function on all of $\mathbb N$, yet only the values $b(0),\dots,b(n)$ appear in the product; the remaining values are unconstrained junk. Consequently the existential over $b$ is equivalent to an existential over the finite tuple $(b(0),\dots,b(n))$ of natural numbers.

Degenerate cases. Taking $n=0$ and $b(0)=0$ makes the product the identity, so the identity map of $[0,1]$ has this property; the property is therefore not vacuous. Taking $n=0$ and $b(0)=m$ gives the $m$-fold composite $A^{m}$, so every nonnegative power of $A$ has the property.

What is asserted is an equality of group elements only. The property says that $f$ equals some such product; it does not, of itself, state that $f$ lies in any particular subgroup, that the representation is unique, that the exponents are determined by $f$, or that $n$ is minimal.