Read-back: a bundle of definitions

This file introduces no theorems about the objects listed below; it introduces the objects themselves. What follows is, for each one, exactly what it says of its argument.

Standing conventions used throughout

The real line. $\mathbb{R}$ carries its usual linear order.

The unit interval as a type. Write

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

and regard $I$ as a type whose elements are pairs consisting of a real number $x$ together with a proof that $0 \le x \le 1$. Two such elements are compared by comparing the underlying real numbers: $z \le w$ in $I$ means exactly $z \le w$ in $\mathbb{R}$. So $I$ is the closed interval $[0,1]$ with the order inherited from $\mathbb{R}$, and it is the same set as the standard unit interval of the ambient library. Whenever an element of $I$ appears in a formula about real numbers below, it is the underlying real number that is meant.

Order isomorphism. For linearly ordered sets $X$ and $Y$, an order isomorphism $f : X \to Y$ is a bijection such that

$$f(a) \le f(b) \iff a \le b \qquad\text{for all } a, b \in X .$$

This is the whole of the data: a bijection together with that two-sided equivalence. In particular no continuity, differentiability or piecewise structure is part of the notion, and nothing is postulated about $f$ beyond bijectivity and that equivalence. (For $X = Y = \mathbb{R}$ continuity and strict monotonicity are nevertheless automatic consequences of the definition, not extra hypotheses; the same holds for $X = Y = [0,1]$. This is a consequence, not something the definitions below say.) I write $f^{-1}$ for the inverse order isomorphism.

The group of order isomorphisms. The order isomorphisms of a fixed linearly ordered set $X$ onto itself form a group: the product $f \cdot g$ is the composite $x \mapsto f(g(x))$, the identity element is the identity map, and the inverse is the inverse map. Two such groups occur below: the order isomorphisms of $\mathbb{R}$, and the order isomorphisms of $[0,1]$.

Powers of two. Two different powers of $2$ occur. In the dyadic-rational definition the exponent is a natural number $k \ge 0$ and $2^k \in \{1, 2, 4, 8, \dots\}$. In the slope conditions the exponent is an integer $n$, possibly negative, and $2^n$ is the corresponding integer power of the real number $2$; every such $2^n$ is strictly positive, and $n$ may be $0$, giving slope $1$.

Finite breakpoint sets. A "finite set $B$ of reals" below means a finite set in the strict sense — a listable, duplicate-free finite collection. It is allowed to be empty.

---

1. Dyadic rationals

For a real number $x$, the condition "$x$ is dyadic" says:

there exist an integer $m$ and a natural number $k$ such that $x = m / 2^{k}$.

Both $m$ and $k$ are existentially quantified inside the condition; $k \ge 0$, so only non-negative powers of $2$ appear in the denominator, and $m$ may be negative or zero. Taking $k = 0$ shows every integer satisfies the condition, and $m = 0$ shows $0$ does. So the condition holds of exactly the dyadic rationals $m/2^{k}$, and it is a condition on an arbitrary real number (not on a number already known to be rational).

---

2. The line model: "$f$ is a Thompson map of the line"

Let $f$ be an order isomorphism of $\mathbb{R}$ onto itself. The condition "$f$ is a Thompson map of the line" is the conjunction of three clauses:

(i) for every real $x$ with $x \le 0$, $\;f(x) = x$;

(ii) for every real $x$ with $1 \le x$, $\;f(x) = x$;

(iii) there exists a finite set $B \subseteq \mathbb{R}$ such that

• (iii-a) every element $b \in B$ is dyadic in the sense of §1, and
• (iii-b) for all real numbers $x, y$ with $x < y$ and

$$(x,y) \cap B = \varnothing ,$$

there exist an integer $n$ and a real number $c$ such that

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

Points to note about what this does and does not say.

The fixing clauses are on the closed rays. Clause (i) is stated for $x \le 0$, not $x < 0$, and clause (ii) for $1 \le x$, not $1 < x$. Instantiating them at $x = 0$ and $x = 1$ gives $f(0) = 0$ and $f(1) = 1$ as part of the condition.

The avoidance hypothesis is on the open interval, the conclusion on the closed one. The hypothesis in (iii-b) is that the open interval $(x,y)$ misses $B$; the endpoints $x$ and $y$ may themselves lie in $B$. The conclusion asserts the single affine formula $f(z) = 2^{n}z + c$ on the closed interval $[x,y]$, endpoints included. So at a point of $B$ that is an endpoint of two such intervals, the two affine formulas are each asserted to hold at that point.

The quantification over $x, y$ is over all of $\mathbb{R}$. Nothing confines $x$ and $y$ to $[0,1]$; they range over all reals with $x < y$, so intervals straddling $0$, or lying entirely to the left of $0$, or containing $[0,1]$, are all included.

The slope and intercept may depend on the interval. The integer $n$ and the real $c$ are quantified inside the "for all $x,y$", so different intervals may receive different $n$ and $c$; only the finite set $B$ is chosen once and for all.

The slope is an integer power of two, hence strictly positive. Slope $0$ and negative slopes are excluded; slopes $\tfrac12, \tfrac14, \dots$ are permitted, since $n$ may be negative.

The intercept is an unconstrained real number. The condition places no requirement on $c$ — not dyadicity, not rationality. Nothing in this file asserts that $c$ must be dyadic.

$B$ is not pinned down as "the breakpoints". The condition only asks for some finite dyadic set with property (iii-b). It does not say that $f$ actually fails to be affine at any point of $B$, nor that $B$ is minimal, nor that $B \subseteq [0,1]$. Any finite dyadic superset of a working $B$ works as well.

The empty $B$ is allowed, and forces the identity. If one takes $B = \varnothing$ the avoidance hypothesis is satisfied by every pair $x < y$, so (iii-b) then requires $f$ to be given by one affine formula on every closed interval, hence globally affine; together with clause (i) that forces $f$ to be the identity map. So the witness $B$ can be empty only for $f = \mathrm{id}$.

---

3. The interval model: "$f$ is a Thompson map of $[0,1]$"

Let $f$ be an order isomorphism of $[0,1]$ onto itself. The condition "$f$ is a Thompson map of $[0,1]$" says:

there exists a finite set $B \subseteq \mathbb{R}$ such that every $b \in B$ is dyadic, and such that for all $x, y \in [0,1]$ with $x < y$ and $(x,y) \cap B = \varnothing$, there exist an integer $n$ and a real number $c$ with

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

Here $x$, $y$ and $z$ are elements of the type $I$, and the inequalities $x < y$, $x \le z \le y$ and the equation are all read among the underlying real numbers; $f(z)$ is likewise read as the real number underlying the value.

Points to note.

There is no fixing clause. Unlike §2, this condition has no analogue of clauses (i) and (ii). None is stated. (That $f(0) = 0$ and $f(1) = 1$ holds anyway for every order isomorphism of $[0,1]$, since such a map must carry the least element to the least element and the greatest to the greatest, is a consequence of the ambient notion and not something this condition says.)

Everything said in §2 about $B$, about the open-versus-closed intervals, about the interval-dependence of $n$ and $c$, about the positivity of $2^{n}$, and about the intercept $c$ being an unconstrained real, applies verbatim here. In particular the condition places no dyadicity requirement on $c$, and this file states nothing to that effect for this model.

$B$ is a finite set of reals, not of points of $[0,1]$. It may contain points outside $[0,1]$; those simply never obstruct the avoidance hypothesis, since $(x,y) \subseteq [0,1]$.

The affine conclusion is asserted only at points of $[0,1]$. The variable $z$ ranges over $I$, so the formula is claimed at the points of $[x,y]$ — which, since $x,y \in [0,1]$, is all of $[x,y]$ anyway.

The empty $B$ is again allowed and again forces the identity, by the argument of §2 applied on $[0,1]$: a single affine formula on all of $[0,1]$ with $f(0)=0$ and $f(1)=1$ is the identity.

---

4. Extension by the identity, at the level of bare maps

Given any function $f$ from $I$ to $I$ — no monotonicity, injectivity or surjectivity is required of it — and given a real number $x$, the extension of $f$ evaluated at $x$ is the real number

$$\widetilde{f}(x) \;=\; \begin{cases} f(x) & \text{if } 0 \le x \le 1,\\[2pt] x & \text{otherwise.}\end{cases}$$

This is a total function $\mathbb{R} \to \mathbb{R}$, defined by cases on whether $x$ lies in $[0,1]$; on $[0,1]$ its value is the real number underlying $f(x)$, and off $[0,1]$ it is $x$ itself. The case distinction is made using the decidability of the membership $x \in [0,1]$ supplied by classical logic, so the definition is not an algorithm.

---

5. Extension by the identity, as an order isomorphism of the line

Given an order isomorphism $f$ of $[0,1]$, the extension of $f$ is the order isomorphism of $\mathbb{R}$ whose

• forward map is $\widetilde{f}$ of §4 applied to the underlying function of $f$, and
• inverse map is $\widetilde{\,\cdot\,}$ of §4 applied to the underlying function of $f^{-1}$.

Concretely it is the map

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

packaged together with proofs that this map is a bijection of $\mathbb{R}$ with the stated inverse and that $a \le b \iff \widetilde{f}(a) \le \widetilde{f}(b)$. Those three facts are established as part of the construction — they are the content the packaging carries — and the resulting object is by construction an element of the group of order isomorphisms of $\mathbb{R}$. It is recorded separately that the value of the extension at a real number $x$ is literally $\widetilde{f}(x)$.

---

6. Restriction to $[0,1]$

This construction takes three arguments:

1. an order isomorphism $L$ of $\mathbb{R}$ onto itself;
2. a proof that $L(x) = x$ for every real $x$ with $x \le 0$;
3. a proof that $L(x) = x$ for every real $x$ with $1 \le x$.

Both hypotheses are on the closed rays, and both are required: the construction is not defined for an $L$ lacking them. From them, instantiated at $x = 0$ and $x = 1$, one gets $L(0) = 0$ and $L(1) = 1$, and hence also $L^{-1}(0) = 0$ and $L^{-1}(1) = 1$.

The result is the order isomorphism of $[0,1]$ onto itself given by

$$z \;\longmapsto\; L(z), \qquad \text{with inverse } \quad z \;\longmapsto\; L^{-1}(z).$$

That both of these land in $[0,1]$ — i.e. that $0 \le L(z) \le 1$ and $0 \le L^{-1}(z) \le 1$ whenever $0 \le z \le 1$ — is established in the course of the construction, from $L(0) = 0$, $L(1) = 1$ and the order-preservation of $L$ and $L^{-1}$; so are the two inverse identities and the equivalence $z \le w \iff L(z) \le L(w)$.

It is recorded separately that the underlying real number of the value of the restriction at $z \in [0,1]$ is literally $L(z)$.

Only $L(0) = 0$ and $L(1) = 1$ are actually used; the two hypotheses as stated are stronger than that, and the construction's value does not otherwise depend on them.

---

7. The group $F$ (interval model)

$F$ is defined to be

$$F \;=\; \big\langle\, \{\, f \;:\; f \text{ is a Thompson map of } [0,1] \,\} \,\big\rangle ,$$

the subgroup generated by the set of all order isomorphisms of $[0,1]$ satisfying the condition of §3. Precisely: it is the intersection of all subgroups of the group of order isomorphisms of $[0,1]$ that contain that set — equivalently, the set of all finite products $g_1^{\pm 1} g_2^{\pm 1} \cdots g_r^{\pm 1}$ with $r \ge 0$ and each $g_i$ satisfying the condition of §3, the empty product being the identity map.

What is thereby asserted about the set $S = \{\, f : f \text{ is a Thompson map of } [0,1] \,\}$:

• that $F$ is a subgroup of the group of order isomorphisms of $[0,1]$ — closed under composition and inverses, and containing the identity;
• that $S \subseteq F$, i.e. every map satisfying the condition of §3 is a member of $F$. This is recorded explicitly as a statement in its own right.

What is not thereby asserted:

• not that $S$ is itself closed under composition, or under inverses, or that it contains the identity map;
• not that $S$ is a subgroup;
• not that $F = S$, i.e. not that every member of $F$ satisfies the condition of §3. The definition leaves open that $F$ is strictly larger than $S$. The converse inclusion $F \subseteq S$ is not stated anywhere in this file.

So "a member of $F$" is, on the strength of this file alone, a strictly weaker predicate than "satisfies the condition of §3" (weaker in the sense of being implied by it, with the reverse implication unproved here).

---

8. The group of the line model

$F_{\text{line}}$ is defined in exactly the same way, one level up:

$$F_{\text{line}} \;=\; \big\langle\, \{\, f \;:\; f \text{ is a Thompson map of the line} \,\} \,\big\rangle ,$$

the subgroup of the group of order isomorphisms of $\mathbb{R}$ generated by the set of all order isomorphisms of $\mathbb{R}$ satisfying the three-clause condition of §2 — i.e. the intersection of all subgroups of that group containing that set, equivalently all finite products of such maps and their inverses.

Everything said in §7 about what is and is not asserted applies here word for word, with §3 replaced by §2. In particular it is asserted that every map satisfying the condition of §2 is a member of $F_{\text{line}}$ (this is recorded explicitly), and it is not asserted that the set of such maps is closed under composition or inverses, nor that every member of $F_{\text{line}}$ satisfies the condition of §2.

---

9. Triviality near $0$

For an order isomorphism $f$ of $[0,1]$, the condition "$f$ is trivial near $0$" says:

there exists a real number $\varepsilon$ with $\varepsilon > 0$ such that every $z \in [0,1]$ with $z < \varepsilon$ satisfies $f(z) = z$.

So $f$ fixes every point of $[0,\varepsilon) \cap [0,1]$ pointwise, the inequality being the strict one $z < \varepsilon$.

Notes. The quantifier on $\varepsilon$ is $\exists$, and $\varepsilon$ is not required to be at most $1$; a witness $\varepsilon > 1$ is permitted, and such a witness would make the condition say that $f(z) = z$ for every $z \in [0,1]$, i.e. that $f$ is the identity. The condition is satisfied by the identity map (any $\varepsilon$ works), so it is not vacuous. The point $z = 0$ always satisfies $z < \varepsilon$, so $f(0) = 0$ is among the assertions (though it holds for every order isomorphism of $[0,1]$ anyway).

---

10. Triviality near $1$

For an order isomorphism $f$ of $[0,1]$, the condition "$f$ is trivial near $1$" says:

there exists a real number $\varepsilon$ with $\varepsilon > 0$ such that every $z \in [0,1]$ with $1 - \varepsilon < z$ satisfies $f(z) = z$.

So $f$ fixes every point of $(1-\varepsilon, 1] \cap [0,1]$ pointwise. The inequality $1 - \varepsilon < z$ is strict, and the endpoint $z = 1$ is included (it always satisfies the inequality), so $f(1) = 1$ is among the assertions.

As in §9, $\varepsilon$ is not bounded above; a witness $\varepsilon > 1$ is permitted, and would force $f$ to be the identity on all of $[0,1]$. The identity map satisfies the condition.

---

11. The support of a map of $[0,1]$

For an order isomorphism $f$ of $[0,1]$, the support of $f$ is defined as a subset of $\mathbb{R}$, namely

$$\operatorname{supp} f \;=\; \{\, t \in \mathbb{R} \;:\; \exists\, z \in [0,1] \text{ with } z = t \text{ and } f(z) \ne t \,\} .$$

Because a point of $[0,1]$ is determined by the real number underlying it, the existential is witnessed by at most one $z$, and the set is therefore exactly

$$\operatorname{supp} f \;=\; \{\, t \in [0,1] \;:\; f(t) \ne t \,\},$$

the set of points of $[0,1]$ that $f$ moves. It is a subset of $[0,1]$: a real number outside $[0,1]$ never belongs to it, whatever $f$ does.

No closure is taken. This is the bare moved-point set, not its topological closure. It is empty precisely when $f$ is the identity map, and it does not contain $0$ or $1$ (those are fixed by every order isomorphism of $[0,1]$).

---

12. The map $A$

$A$ is defined as the restriction (§6) to $[0,1]$ of a particular order isomorphism $\alpha$ of $\mathbb{R}$. That $\alpha$ is defined by a nest of case distinctions; computing them out, the value of $\alpha$ at a real number $x$ is:

$$\alpha(x) \;=\; \begin{cases} x & x \le 0,\\[2pt] \tfrac{1}{2}x & 0 < x \le \tfrac12,\\[2pt] x - \tfrac14 & \tfrac12 < x \le \tfrac34,\\[2pt] 2x - 1 & \tfrac34 < x \le 1,\\[2pt] x & 1 < x . \end{cases}$$

The formulas agree at the four cut points, so the same function may equivalently be described on closed pieces: $\alpha$ is the identity on $(-\infty, 0]$, equals $\tfrac12 x$ on $[0,\tfrac12]$, equals $x - \tfrac14$ on $[\tfrac12, \tfrac34]$, equals $2x-1$ on $[\tfrac34, 1]$, and is the identity on $[1,\infty)$. (Check: at $x=0$ both give $0$; at $x = \tfrac12$ both give $\tfrac14$; at $x = \tfrac34$ both give $\tfrac12$; at $x=1$ both give $1$.) It is established that $\alpha$ is strictly increasing and surjective, hence an order isomorphism of $\mathbb{R}$, and that it fixes every point of $(-\infty,0]$ and every point of $[1,\infty)$ — which is what licenses the restriction of §6.

Therefore $A$ is the order isomorphism of $[0,1]$ onto itself given by

$$A(z) \;=\; \begin{cases} \tfrac12 z & 0 \le z \le \tfrac12,\\[2pt] z - \tfrac14 & \tfrac12 \le z \le \tfrac34,\\[2pt] 2z - 1 & \tfrac34 \le z \le 1 . \end{cases}$$

Its breakpoints are $\tfrac12$ and $\tfrac34$; its three slopes are $\tfrac12$, $1$ and $2$; and $A(0) = 0$, $A(\tfrac12) = \tfrac14$, $A(\tfrac34) = \tfrac12$, $A(1) = 1$. Sample interior values: $A(\tfrac14) = \tfrac18$, $A(\tfrac58) = \tfrac38$, $A(\tfrac78) = \tfrac34$. Its inverse is the restriction of $\alpha^{-1}$.

$A$ is introduced as an element of the group of all order isomorphisms of $[0,1]$. Nothing in this file asserts that $A$ satisfies the condition of §3, nor that $A$ belongs to the group $F$ of §7, nor that $A$ together with the map of §13 generates anything.

---

13. The map $B$

$B$ is likewise the restriction (§6) to $[0,1]$ of a particular order isomorphism $\beta$ of $\mathbb{R}$, whose value at a real number $x$, with the case distinctions computed out, is:

$$\beta(x) \;=\; \begin{cases} x & x \le \tfrac12,\\[2pt] \tfrac12 x + \tfrac14 & \tfrac12 < x \le \tfrac34,\\[2pt] x - \tfrac18 & \tfrac34 < x \le \tfrac78,\\[2pt] 2x - 1 & \tfrac78 < x \le 1,\\[2pt] x & 1 < x . \end{cases}$$

Note that the first clause is $x \le \tfrac12$, so $\beta$ is the identity on the whole ray $(-\infty, \tfrac12]$ — in particular on all of $(-\infty, 0]$, which is how the left-hand hypothesis of §6 is met. Again the formulas agree at the cut points ($\tfrac12 \mapsto \tfrac12$; $\tfrac34 \mapsto \tfrac58$; $\tfrac78 \mapsto \tfrac34$; $1 \mapsto 1$), so $\beta$ may equivalently be described on closed pieces: the identity on $(-\infty, \tfrac12]$, $\tfrac12 x + \tfrac14$ on $[\tfrac12, \tfrac34]$, $x - \tfrac18$ on $[\tfrac34, \tfrac78]$, $2x-1$ on $[\tfrac78, 1]$, the identity on $[1,\infty)$. It is established that $\beta$ is strictly increasing and surjective, hence an order isomorphism of $\mathbb{R}$, and that it fixes $(-\infty, 0]$ and $[1,\infty)$ pointwise.

Therefore $B$ is the order isomorphism of $[0,1]$ onto itself given by

$$B(z) \;=\; \begin{cases} z & 0 \le z \le \tfrac12,\\[2pt] \tfrac12 z + \tfrac14 & \tfrac12 \le z \le \tfrac34,\\[2pt] z - \tfrac18 & \tfrac34 \le z \le \tfrac78,\\[2pt] 2z - 1 & \tfrac78 \le z \le 1 . \end{cases}$$

So $B$ is the identity on $[0,\tfrac12]$ and moves only points of $(\tfrac12, 1)$. Its breakpoints are $\tfrac12$, $\tfrac34$, $\tfrac78$; its four slopes are $1$, $\tfrac12$, $1$ and $2$; and $B(\tfrac12) = \tfrac12$, $B(\tfrac34) = \tfrac58$, $B(\tfrac78) = \tfrac34$, $B(1) = 1$. Sample values: $B(\tfrac14) = \tfrac14$, $B(\tfrac58) = \tfrac{9}{16}$, $B(\tfrac{13}{16}) = \tfrac{11}{16}$, $B(\tfrac{15}{16}) = \tfrac78$.

As with $A$, nothing in this file asserts that $B$ satisfies the condition of §3, that $B$ belongs to $F$, or that $A$ and $B$ generate anything.