Read-back: exists_mulEquiv_support_subgroup

The objects the statement is built from

Everything below is stated for the real numbers with their usual order.

Dyadic numbers. A real number $x$ is called dyadic when there are an integer $m$ and a natural number $k$ (so $k \ge 0$) with

$$x = \frac{m}{2^{k}}.$$

Nothing further is required of $m$ or $k$. The numerator ranges over all integers, so $0$, every negative dyadic, and every integer are dyadic.

The unit interval as a type. Write

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

regarded as a set in its own right and carrying the order it inherits from $\mathbb{R}$.

Order isomorphisms of $I$. An order isomorphism of $I$ is a bijection $f : I \to I$ together with the property that for all $x, y \in I$,

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

Equivalently: a bijection of $I$ that is strictly increasing and whose inverse is strictly increasing. No continuity is required of $f$: this is an isomorphism of ordered sets, not a homeomorphism, and no topology enters the statement. These maps form a group $\operatorname{Aut}_{\le}(I)$ under composition: the product $f \cdot g$ is the map $x \mapsto f(g(x))$, the identity element is $x \mapsto x$, and the inverse of $f$ is its inverse bijection.

The piecewise-linearity condition. Say that an order isomorphism $f$ of $I$ is Thompson-like when there exists a finite set $B \subseteq \mathbb{R}$ such that

1. every element of $B$ is dyadic; and
2. for all $x, y \in I$ with $x < y$ and with

$$(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 I \text{ with } x \le z \le y.$$

Several details of this condition matter.

• The finite set $B$ is a set of real numbers; it is not required to be contained in $[0,1]$, and it is allowed to be empty — in which case $f$ must be given by a single formula $2^{n}z + c$ on all of $[0,1]$.
• The gap condition is imposed on the open interval $(x,y)$, while the affine formula is demanded on the closed interval $[x,y]$. So the formula is pinned down at the endpoints $x$ and $y$ as well, not merely strictly between them.
• The exponent $n$ ranges over all integers — positive, zero and negative — so the slope $2^{n}$ is an arbitrary integer power of $2$; it is in particular always strictly positive. The pair $(n, c)$ is chosen after $x$ and $y$, so it may differ from one gap to the next.
• The intercept $c$ is an arbitrary real number. Nothing in this condition requires $c$ to be dyadic.
• The set $B$ is existentially quantified: it is a witnessing breakpoint set, not canonically attached to $f$, and a given $f$ may satisfy the condition with many different $B$.

The group $\mathcal{F}$. Let

$$\mathcal{F} = \big\langle\, \{\, f \in \operatorname{Aut}_{\le}(I) : f \text{ is Thompson-like} \,\} \,\big\rangle,$$

the subgroup of $\operatorname{Aut}_{\le}(I)$ generated by the Thompson-like order isomorphisms — that is, the smallest subgroup of $\operatorname{Aut}_{\le}(I)$ containing all of them, equivalently the set of all finite products of Thompson-like maps and their inverses.

It is worth being explicit that $\mathcal{F}$ is defined as this generated subgroup, not as the set of Thompson-like maps itself. So "$g \in \mathcal{F}$" means, as far as this statement is concerned, only that $g$ is such a finite product. Nothing here asserts that the set of Thompson-like maps is already closed under composition and inverses, and nothing here asserts that every element of $\mathcal{F}$ is itself Thompson-like.

The moved-point set. For an order isomorphism $f$ of $I$, put

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

which is to say

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

the set of points of $[0,1]$ that $f$ actually moves, viewed as a subset of $\mathbb{R}$.

No closure is taken. This is the bare moved-point set, not its topological closure. (In dynamics "support" frequently denotes the closure of this set; that is not what is meant here.) Note also that $\operatorname{supp}(f) \subseteq [0,1]$ holds automatically, since every element of the set is by construction a point of $[0,1]$.

What the statement asserts

Let $a$ and $b$ be real numbers, and suppose

• $0 \le a$;
• $a < b$ (strictly);
• $b \le 1$;
• $a$ is dyadic;
• $b$ is dyadic.

Suppose further that we are given an integer $k$ — universally quantified, so there is one instance of the claim for each such $k$ — satisfying

$$b - a = 2^{k},$$

where $2^{k}$ is the integer power of $2$ in $\mathbb{R}$, so that $2^{k} = 1/2^{-k}$ when $k < 0$ and fractional lengths are allowed. Since the first three hypotheses give $b - a \le 1$, the exponent $k$ is forced to satisfy $k \le 0$. Taken together, the hypotheses on $a$, $b$ and $k$ say exactly that $[a,b]$ is a non-degenerate closed subinterval of $[0,1]$ with dyadic endpoints whose length is an integer power of two.

Then the assertion is:

There exists a subgroup $H$ of $\mathcal{F}$ such that

1. (exact characterisation) for every $g \in \mathcal{F}$,

$$g \in H \iff \operatorname{supp}(g) \subseteq [a,b],$$

the interval $[a,b] = \{t \in \mathbb{R} : a \le t \le b\}$ being closed at both ends; and 2. (abstract isomorphism) the collection of group isomorphisms from $H$ to $\mathcal{F}$ is non-empty — i.e. there exists at least one bijection $\varphi : H \to \mathcal{F}$ satisfying $\varphi(g h) = \varphi(g)\,\varphi(h)$ for all $g, h \in H$.

Clause 1 is a two-way equivalence, not an implication in either direction alone, so it pins the underlying set of $H$ down completely: $H$ is exactly

$$\{\, g \in \mathcal{F} : \operatorname{supp}(g) \subseteq [a,b] \,\}.$$

Because a subgroup is determined by its underlying set, the subgroup $H$ whose existence is asserted is unique. The force of the existential in clause 1 is therefore the assertion that this set is a subgroup of $\mathcal{F}$ — closed under composition and inverses, and containing the identity.

Clause 2 asserts only that some isomorphism exists. It is a bare existence statement carrying no chosen map: no particular isomorphism is named, constructed or characterised, and the isomorphism is not claimed to be related in any way to the inclusion of $H$ into $\mathcal{F}$.

Precision points and degenerate cases

The subgroup lives inside $\mathcal{F}$, and is compared with all of $\mathcal{F}$. The elements of $H$ are elements of $\mathcal{F}$, so $H \subseteq \mathcal{F}$; clause 2 nevertheless asserts that $H$ is abstractly isomorphic to the whole of $\mathcal{F}$. Whether $H$ is a proper subgroup is not addressed either way.

The interval is closed, so the endpoints may be moved. Since the required containment is $\operatorname{supp}(g) \subseteq [a,b]$ and not $\subseteq (a,b)$, an element of $H$ is permitted to move the points $a$ and $b$ themselves. What it is forbidden to move is every point of $[0,1]$ lying strictly outside $[a,b]$, i.e. every point of $[0,a) \cup (b,1]$.

Nothing requires an element of $H$ to move anything. The condition is a containment of the moved-point set, so the identity map lies in $H$ for every $a$ and $b$, and an element of $H$ may fix points of $[a,b]$ freely — including all of them.

The degenerate instance $a = 0$, $b = 1$, $k = 0$ is included. These values satisfy every hypothesis: $0 \le 0$, $0 < 1$, $1 \le 1$, both endpoints are dyadic, and $1 - 0 = 1 = 2^{0}$. But $\operatorname{supp}(g) \subseteq [0,1]$ holds for every order isomorphism $g$ of $I$, as noted above. So for these values the condition in clause 1 is satisfied vacuously by every $g$, the unique $H$ it specifies is $\mathcal{F}$ itself, and clause 2 reduces to the assertion that $\mathcal{F}$ is isomorphic to $\mathcal{F}$. The statement's family of instances therefore contains one that says nothing.

The hypotheses are satisfiable, and satisfiable non-degenerately. Beyond $a = 0$, $b = 1$, $k = 0$, the values $a = 1/2$, $b = 3/4$, $k = -2$ satisfy all six hypotheses. So no hypothesis, and no combination of them, is impossible to meet.

The isomorphism is purely group-theoretic. Clause 2 speaks of a bijection preserving multiplication. It says nothing about the isomorphism preserving order, preserving or transporting moved-point sets, being continuous, being implemented by conjugation in any larger group, or being induced by an affine rescaling of the interval.

The integer $k$ carries no independent content beyond the equation. It appears in the statement only through the hypothesis $b - a = 2^{k}$; since $a$ and $b$ determine $k$ uniquely when such a $k$ exists, quantifying over $k$ with this hypothesis amounts to requiring that $b - a$ be an integer power of $2$.

Everything is stated for a single fixed pair $(a,b)$. The claim is made separately for each admissible $a$, $b$ and $k$. No relation between the subgroups obtained for different intervals is asserted, and no compatibility between the different isomorphisms is asserted.