Read-back: the statement isPositive_mul

The ambient group

Let $I = [0,1]$ denote the closed real unit interval, carrying the order it inherits from $\mathbb{R}$.

Let

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

be the set of order isomorphisms of $I$ onto itself: bijections of $I$ that reflect as well as preserve the order. No continuity, differentiability, piecewise-linearity or dyadic condition is built into $G$; membership in $G$ is exactly "order-preserving bijection of $[0,1]$".

$G$ is a group under the operation

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

i.e. the product of two elements is their composite with the right-hand factor applied first; the identity element $1$ is the identity map of $I$, and the inverse is the inverse map. Powers are the iterated products in this group: $f^0 = 1$ and $f^{k+1} = f^k \cdot f$, so $f^k$ is the $k$-fold composite of $f$ with itself, and $f^{-k}$ denotes $(f^k)^{-1}$.

All products written below are products in this group, so in every juxtaposition the rightmost factor acts first.

Two distinguished elements

Two specific elements $A, B \in G$ are singled out. Each is given by a monotone piecewise-affine formula; the formulas agree at the shared endpoints of the listed intervals, so each is a well-defined increasing bijection of $[0,1]$ fixing $0$ and $1$.

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

(Both are obtained by first defining an increasing bijection of all of $\mathbb{R}$ that is the identity outside $[0,1]$ and is given by the formulas above on $[0,1]$, and then restricting it to $[0,1]$. The restriction is what $A$ and $B$ denote here.)

The distinguished family $X_0, X_1, X_2, \dots$

For every natural number $n \ge 0$ an element $X_n \in G$ is defined by

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

the product again being composition with the rightmost factor first: $X_{n+1}(x) = A^{-n}\bigl(B(A^{n}(x))\bigr)$. In particular $X_1 = B$ (the $n = 0$ case, where $A^0 = 1$), and for $n \ge 1$ the element $X_{n+1}$ is the conjugate $A^{-1} X_n A$.

Positive words

For a finite list of natural numbers $(c_0, c_1, \dots, c_{n-1})$ — length $n \ge 0$, entries $c_i \in \mathbb{N}$ — define an element of $G$ by

$$w(c_0, c_1, \dots, c_{n-1}) \;=\; X_0^{\,c_0}\, X_1^{\,c_1}\, X_2^{\,c_2} \cdots X_{n-1}^{\,c_{n-1}}.$$

Three points of precision about this definition:

• The index is tied to the position in the list. The recursion starts at index $0$ and advances the index by exactly one for each entry consumed, so the $k$-th entry of the list is always the exponent of $X_k$. Reading the list left to right therefore gives the factors in order of strictly increasing index, and the product is taken in that order — with, as always here, the rightmost (highest-index) factor acting on a point first.
• The exponents are natural numbers: each $c_i$ satisfies $c_i \ge 0$. Zero exponents are permitted, and a factor $X_k^{0}$ is the identity, so an index may in effect be skipped. Negative exponents are not expressible: no inverse $X_k^{-1}$ can occur as a factor.
• The empty list ($n = 0$) is allowed, and $w() = 1$, the identity element of $G$.

Call an element $f \in G$ positive if there exists at least one such finite list of natural numbers realising it:

$$f \text{ is positive} \iff \exists\, n \ge 0,\ \exists\, c_0,\dots,c_{n-1} \in \mathbb{N} :\; f = X_0^{\,c_0} X_1^{\,c_1} \cdots X_{n-1}^{\,c_{n-1}}.$$

The list is not required to be unique, nor reduced, nor minimal in any sense; mere existence of one list is the whole condition.

Because zero exponents delete a factor, the set of positive elements can equivalently be described as

$$\bigl\{\, X_{i_1}^{\,e_1} X_{i_2}^{\,e_2} \cdots X_{i_k}^{\,e_k} \;:\; k \ge 0,\; i_1 < i_2 < \cdots < i_k,\; e_j \ge 1 \,\bigr\},$$

that is: finite products of the $X_i$ with strictly increasing indices (the indices need not form an initial segment of $\mathbb{N}$, and gaps are allowed) and with no inverses of any $X_i$ appearing. The identity element is positive, via the empty list (equivalently, via any list all of whose entries are $0$).

The assertion

For every pair of elements $f, g$ of $G$ — that is, every pair of order isomorphisms of $[0,1]$ onto itself — if $f$ is positive and $g$ is positive, then the product $f \cdot g$, the map $x \mapsto f(g(x))$, is positive.

Spelled out with all quantifiers: for all $f, g \in G$, if there exist a finite list $(a_0,\dots,a_{m-1})$ of natural numbers with $f = X_0^{a_0} \cdots X_{m-1}^{a_{m-1}}$ and a finite list $(b_0,\dots,b_{n-1})$ of natural numbers with $g = X_0^{b_0} \cdots X_{n-1}^{b_{n-1}}$, then there exists a finite list $(c_0,\dots,c_{p-1})$ of natural numbers with

$$f \cdot g \;=\; X_0^{\,c_0} X_1^{\,c_1} \cdots X_{p-1}^{\,c_{p-1}}.$$

The two elements $f$ and $g$ are arguments that are recovered from the two hypotheses rather than supplied separately; apart from those two hypotheses the assertion carries no further assumptions of any kind — in particular no hypothesis that $f$ or $g$ be piecewise linear, dyadic, or a member of any previously named subgroup, and no structural assumption relating the two witnessing lists.

Degenerate and edge cases included

• The hypotheses are satisfiable, not vacuous: the identity, $A = X_0$, $B = X_1$, every $X_i$, and every finite product of the kind described, are positive.
• The case $f = 1$ or $g = 1$ (empty witnessing list, or a list of zeros) is included.
• Because the exponents range over $\mathbb{N}$, the case where every exponent of one or both witnessing lists is $0$ is included, and no case with a negative exponent arises.
• No bound is asserted on the length $p$ of the resulting list, and no relation between $p$ and the lengths $m$, $n$ of the two given lists is asserted.
• The order of the factors matters in the conclusion: the assertion is about the composite that applies $g$ first and then $f$.