Read-back: the declaration mem_commutator_iff

0. Setting: the objects the statement is about

The interval, as an ordered set. Let

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

regarded as a set of real numbers and ordered by the order it inherits from $\mathbb{R}$: for $x, y \in I$, $x \le y$ means exactly $x \le y$ in $\mathbb{R}$. Throughout, an element of $I$ is silently identified with the real number it is, and the statements below about elements of $I$ are equations and inequalities between real numbers.

The ambient group. Let

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

be the set of order isomorphisms of $I$ onto itself. Note carefully what this does and does not require: $f$ is a bijection of $I$ and the displayed equivalence holds. No continuity, differentiability or measurability of $f$ is assumed anywhere, and no topology on $I$ is used in any of the definitions below; the neighbourhood conditions in §3 are stated by hand with explicit constants, not through a topology.

$G$ is made a group by composition: the product $f_1 f_2$ is the map $z \mapsto f_1\bigl(f_2(z)\bigr)$ — the left factor is applied last. The identity element is the identity map of $I$, and $f^{-1}$ is the inverse bijection.

1. The generating condition

Say that $f \in G$ is admissible if the following holds:

There exists a finite set $B \subseteq \mathbb{R}$ such that

1. every $b \in B$ is a dyadic rational, i.e. $b = m/2^{k}$ for some integer $m \in \mathbb{Z}$ and some natural number $k \ge 0$; and
2. for every pair $x, y \in I$ with $x < y$ and

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

(the open real interval between $x$ and $y$ meets $B$ in no point), there exist an integer $n \in \mathbb{Z}$ and a real number $c \in \mathbb{R}$ such that

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

Several points of this condition are worth spelling out, since they are part of what the declaration asserts.

• The affine formula is demanded on the closed interval $[x,y]$, endpoints included, even though only the open interval $(x,y)$ is required to avoid $B$.
• The exponent $n$ and the constant $c$ are quantified inside, after $x$ and $y$: they may depend on the pair $(x,y)$. The slope is $2^{n}$ with $n$ an arbitrary integer, so it is a positive integer power of $2$ (possibly a negative power, i.e. $2^{-1}, 2^{-2}, \dots$), but it is never negative or zero. The intercept $c$ is an arbitrary real number: nothing here requires $c$ to be dyadic.
• $B$ is a finite set of real numbers, not required to be contained in $[0,1]$; points of $B$ outside $[0,1]$ simply impose nothing.
• $B$ is allowed to be empty, in which case, taking $x = 0$ and $y = 1$, the condition demands a single affine formula $f(z) = 2^{n}z + c$ on all of $[0,1]$.
• Because $x$ and $y$ are required to lie in $I$, the largest interval the condition speaks about is $[0,1]$ itself.

2. The group in question and its derived subgroup

Let

$$F \;=\; \text{the smallest subgroup of } G \text{ containing every admissible } f,$$

that is, the intersection of all subgroups of $G$ that contain the set of admissible maps. Equivalently, $F$ consists of exactly those elements of $G$ expressible as a finite product $f_1^{\pm 1} f_2^{\pm 1} \cdots f_k^{\pm 1}$ with each $f_i$ admissible (the empty product being the identity). $F$ is defined as this generated subgroup; nothing in the declaration asserts that the set of admissible maps is already closed under composition and inversion, or that $F$ consists only of admissible maps.

Let $[F,F]$ denote the derived (commutator) subgroup of the group $F$, formed inside $F$:

$$[F,F] \;=\; \text{the smallest subgroup of } F \text{ containing } \bigl\{\, a b a^{-1} b^{-1} \;:\; a, b \in F \,\bigr\},$$

with the commutator taken in the convention $[a,b] = a b a^{-1} b^{-1}$ and with the product being composition as in §0. Two things about this:

• It is the subgroup generated by the commutators, not the set of commutators. Membership of $g$ in $[F,F]$ means that $g$ is a finite product of commutators of elements of $F$; it does not say that $g$ is a single commutator $aba^{-1}b^{-1}$.
• Both entries $a, b$ range over $F$, and the resulting object is a subgroup of $F$ — not a subgroup of the larger group $G$, and not an intersection of $F$ with some commutator subgroup of $G$.

3. The two triviality conditions

For $f \in G$ define:

(Z) $f$ is trivial near $0$: there exists a real number $\varepsilon$ with $\varepsilon > 0$ such that

$$f(z) = z \qquad \text{for every } z \in I \text{ with } z < \varepsilon .$$

(O) $f$ is trivial near $1$: there exists a real number $\delta$ with $\delta > 0$ such that

$$f(z) = z \qquad \text{for every } z \in I \text{ with } 1 - \delta < z .$$

Points to note:

• (Z) and (O) are two separate existential statements. The constants $\varepsilon$ and $\delta$ are chosen independently; nothing requires them to be equal or related.
• (Z) says $f$ fixes every point of $[0,1] \cap [0,\varepsilon) = [0,\varepsilon)$ for small $\varepsilon$; in particular the point $z = 0$ is included, since $0 < \varepsilon$ always holds. Similarly (O) says $f$ fixes every point of $(1-\delta, 1]$, the endpoint $z = 1$ included.
• Neither $\varepsilon$ nor $\delta$ is required to be at most $1$. This is harmless but worth recording: if $\varepsilon > 1$ then the hypothesis "$z < \varepsilon$" holds for every $z \in [0,1]$, so with such an $\varepsilon$ condition (Z) would say $f$ is the identity map of $[0,1]$. Since $\varepsilon$ is existentially quantified, (Z) is nonetheless the weaker, genuinely local statement: a map satisfying it for some large $\varepsilon$ satisfies it for every smaller one as well.
• The fixing is required of the values of $f$ as real numbers: $f(z)$ and $z$ are compared in $\mathbb{R}$.
• Both (Z) and (O) hold for the identity map, so neither is vacuous or unsatisfiable.

4. The assertion

The declaration asserts:

For every element $g$ of the group $F$: $g \in [F,F] \quad\Longleftrightarrow\quad \bigl(\text{$g$ is trivial near $0$}\bigr) \ \text{ and } \ \bigl(\text{$g$ is trivial near $1$}\bigr),$ i.e. $g$ lies in the derived subgroup of $F$ (as described in §2) if and only if both condition (Z) and condition (O) of §3 hold for the underlying order isomorphism of $[0,1]$ that $g$ is.

Fully unwound, this reads: for every $g \in F$, $g$ belongs to the smallest subgroup of $F$ containing all elements $aba^{-1}b^{-1}$ with $a, b \in F$, if and only if there exist reals $\varepsilon > 0$ and $\delta > 0$ such that $g(z) = z$ for all $z \in [0,1]$ with $z < \varepsilon$ and $g(z) = z$ for all $z \in [0,1]$ with $z > 1 - \delta$.

Binders and hypotheses, accounted for

• One universally quantified variable, $g$, ranging over the elements of the group $F$ (not over all of $G$). An element of $F$ is, formally, a pair consisting of an order isomorphism of $[0,1]$ together with a proof that it lies in $F$; the right-hand side of the biconditional speaks about the order isomorphism part of that pair. There is no separate hypothesis "$g \in F$": that is carried by the type of $g$.
• No other hypotheses of any kind. There are no side conditions, no implicit parameters left to the reader, and no finiteness, continuity, genericity or nondegeneracy assumptions. The only background data are the structural ones described in §0: the order on $[0,1]$ inherited from $\mathbb{R}$, the composition group law on order isomorphisms of $[0,1]$, and the group structure $F$ inherits as a subgroup of that group.
• The claim is a biconditional, in both directions, for each such $g$; it is not an inclusion in one direction only.
• The existential quantifiers in (Z) and (O) are plain existentials ("there exists"), not unique existentials.
• The quantifier order in §1 is: $\exists B$, then ($\forall b \in B$) and ($\forall x, y$, $\exists n, c$, $\forall z$). In particular $B$ is chosen once for $f$, while $n$ and $c$ are chosen after $x$ and $y$.

Degenerate and edge cases the quantifiers include

• $g$ may be the identity element of $F$, for which both sides hold (the identity is the empty product of commutators, and it fixes every point).
• The endpoints $0$ and $1$ of the interval are included in the fixing conditions, as noted in §3.
• The hypothesis "$g$ is an element of $F$" is satisfiable, so the statement is not vacuous.
• The statement says nothing about, and imposes nothing on, elements of $G$ outside $F$.