No two piecewise-linear homeomorphisms with finitely many breakpoints form a free basis (Theorem 3.1: PLF(ℝ) has no free subgroup of rank greater than one)

Proved

BrinSquier.no_free_subgroup_of_rank_two

by dbenbenn · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemsgroup-theorypiecewise-lineartopology

For any two piecewise-linear homeomorphisms $f,g$ of $\mathbb{R}$ with finitely many breakpoints, the homomorphism from the free group of rank two sending its generators to $f$ and $g$ is never injective.

F_2 \longrightarrow \mathrm{PLF}(\mathbb{R}), \qquad a \mapsto f, \quad b \mapsto g\qquad\text{is never injective.}

Equivalently — and this is how Brin and Squier open their Section 3 — any two elements of $\mathrm{PLF}(\mathbb{R})$ satisfy a nontrivial relation: some nonempty reduced word in $f$ , $g$ and their inverses is the identity.

Since a free group of rank greater than one contains one of rank two, and since $\mathrm{PLF}(\mathbb{R})$ is closed under products and inverses, this is exactly their Theorem (3.1): $\mathrm{PLF}(\mathbb{R})$ contains no free subgroup of rank greater than $1$ .

Why it matters. Thompson's group $F$ sits inside $\mathrm{PLF}(\mathbb{R})$ , so $F$ too has no non-abelian free subgroup. Brin and Squier set out to decide whether $F$ is a finitely presented counterexample to von Neumann's conjecture, and called this result half a success: it settles that $F$ cannot be shown non-amenable by exhibiting a free subgroup. Whether $F$ is amenable remains open.

Preamble

import Definitions.Def_BrinSquier
import Mathlib

Formal statement

namespace BrinSquier

theorem no_free_subgroup_of_rank_two (f g : ℝ ≃o ℝ) (hf : IsPLF f) (hg : IsPLF g) :
    ¬ Function.Injective (FreeGroup.lift ![f, g]) := by
  sorry

end BrinSquier

Source

M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. math. 79 (1985), 485-498, https://doi.org/10.1007/BF01388519, p. 494, Theorem (3.1).

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Here $f$ and $g$ are explicit universally quantified arguments of type $\mathbb{R} \simeq_o \mathbb{R}$ — order isomorphisms of the real line, i.e. strictly increasing bijections $\mathbb{R} \to \mathbb{R}$ , forming a group under composition with $(f \cdot g)(x) = f(g(x))$ .

Each of $f$ and $g$ is assumed to satisfy the bundle's non-standard predicate $\mathrm{IsPLF}$ , which unfolds (for $f$ , and identically for $g$ ) to:

\exists\, B \subseteq \mathbb{R} \text{ finite},\ \forall x \in \mathbb{R} \setminus B,\ \exists\, \varepsilon > 0,\ \exists\, a, b \in \mathbb{R},\ \forall y \in (x - \varepsilon,\, x + \varepsilon),\ f(y) = a y + b;

that is, there is a finite exceptional set $B$ of reals such that every point outside $B$ has an open neighbourhood on which $f$ agrees with one affine function, the affine coefficients and the radius depending on the point. The coefficient $a$ is not required to be positive or nonzero by the formula itself, $B$ may be empty, $B$ need not consist of genuine breakpoints, and no condition at all is imposed on $f$ at the points of $B$ . No condition relates $f$ to $g$ ; in particular they may be equal, and either may be the identity map.

Let $F_2$ denote the free group on the two-element index set $\{0, 1\}$ , and let $\varphi : F_2 \to (\mathbb{R} \simeq_o \mathbb{R})$ be the unique group homomorphism determined by

\varphi(x_0) = f, \qquad \varphi(x_1) = g,

where $x_0, x_1$ are the free generators — i.e. $\varphi$ sends a reduced word in $x_0^{\pm 1}, x_1^{\pm 1}$ to the corresponding composite of $f^{\pm 1}$ and $g^{\pm 1}$ .

The conclusion is the negation of injectivity of $\varphi$ as a function $F_2 \to (\mathbb{R} \simeq_o \mathbb{R})$ : it asserts that there exist two distinct elements $w_1 \neq w_2$ of $F_2$ with $\varphi(w_1) = \varphi(w_2)$ . Since $\varphi$ is a group homomorphism, this is equivalently the statement that its kernel is nontrivial: some non-identity reduced word $w$ in two letters evaluates, under $x_0 \mapsto f$ , $x_1 \mapsto g$ , to the identity map of $\mathbb{R}$ . The statement does not exhibit such a word, does not bound its length, and asserts nothing about the subgroup $\langle f, g\rangle$ beyond the failure of this particular map to be one-to-one. Degenerate instances covered by the quantifiers include $f = g$ (where $w = x_0 x_1^{-1}$ lies in the kernel), $f$ or $g$ equal to the identity, and $f, g$ commuting (where the commutator word lies in the kernel); the hypotheses are satisfiable, so the statement is not vacuous.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by dbenbenn · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph