This mission formalizes A. Garrido, An introduction to amenable groups, lecture notes from four talks at the Oxford Advanced Class in Algebra, Michaelmas 2013 (archived PDF) — its Section 1.1, the Banach–Tarski paradox, together with the inclusion $AG \subseteq NF$ that the notes draw from it.

Motivation

The notes open with the theorem that started the subject. In 1924, they recall, Banach and Tarski "proved a remarkable theorem which is nowadays stated as 'given a ball in 3-dimensional space, there is a way of decomposing it into finitely many disjoint pieces that can be rearranged to form two balls of the same size as the original one'" (p. 1). As the notes put it, "This counterintuitive result is essentially a statement about measure theory": no finitely additive, isometry-invariant measure defined on every subset of $\mathbb{R}^3$ can give the unit ball a finite nonzero measure, so Lebesgue measure cannot be extended that way.

The reason is group-theoretic. The free group $F_2$ decomposes paradoxically under its own left multiplication, the rotation group $SO(3,\mathbb{R})$ contains a copy of $F_2$, and a free action transports the decomposition to the sphere; Hausdorff's paradox and a countable correction give the sphere, and radial projection the ball. The same argument shows that a group containing $F_2$ cannot carry an invariant finitely additive probability measure — the inclusion $AG \subseteq NF$ of amenable groups into groups without free subgroups of rank two, whose converse was von Neumann's question.

This mission is the companion of the first Garrido mission, which formalized the measure-theoretic half of Section 1 (equidecomposability, the Banach–Schröder–Bernstein theorem, Tarski's theorem) and Sections 2 and 3.

Setting

A group $G$ acting on a set $X$ makes two subsets $A, B$ $G$-equidecomposable, $A \sim B$, when $A$ can be cut into finitely many pieces which, each moved by one element of $G$, reassemble into $B$; a subset $E \subseteq X$ is $G$-paradoxical when it contains two disjoint proper subsets each equidecomposable with $E$. Both are the published definitions from the first Garrido mission, Equidecomposable and IsParadoxical, and paradoxicality is defined for an arbitrary subset because the notes use it for $\mathbb{S}^2 \setminus D$ and for a ball.

The groups and spaces are the classical ones. $\mathbb{S}^n$ is the unit sphere in $\mathbb{R}^{n+1}$ (Sphere n), with $SO(n+1,\mathbb{R})$ — Mathlib's Matrix.specialOrthogonalGroup — acting by matrix-vector multiplication. $E(3)$ is the group of all isometries of $\mathbb{R}^3$ (EuclideanGroup 3), acting by evaluation; it contains the translations, the rotations and the reflections. A group acts freely (ActsFreely) when no element other than the identity fixes a point. $F_2$ is FreeGroup (Fin 2), and "no free subgroup of rank two" is the published Chou.NoFreeSubgroupOfRankTwo. The rotations $\rho$ and $\sigma$ of Proposition 1.6 are defined in the bundle with their matrices.

Formalization targets

Goal — Corollary 1.10, the Banach–Tarski paradox

Every closed ball of positive radius in $\mathbb{R}^3$, and $\mathbb{R}^3$ itself, is $E(3)$-paradoxical: "Any solid ball in $\mathbb{R}^3$ is $E(3)$-paradoxical. Furthermore, $\mathbb{R}^3$ is $E(3)$-paradoxical" (p. 3).

This is the goal because it is the theorem the section is named for and the one the notes build to.

The path — Propositions 1.5, 1.6 and 1.8, Theorem 1.7, Corollary 1.9

$F_2$ is paradoxical, and so is every nonempty set on which it acts freely (Proposition 1.5); $SO(3,\mathbb{R})$ contains a free group of rank two (Proposition 1.6); the sphere minus a countable set is paradoxical (Theorem 1.7, Hausdorff's paradox); a countable set can be absorbed (Proposition 1.8); so the sphere $\mathbb{S}^n$ is $SO(n+1,\mathbb{R})$-paradoxical for $n \ge 2$ (Corollary 1.9). The steps that the notes state inside proofs are milestones of their own: the two rotations $\rho$ and $\sigma$ generate a free group, a nontrivial rotation fixes exactly two points of $\mathbb{S}^2$, and a countable subset of $\mathbb{S}^2$ has a rotation whose positive powers move it off itself.

Consequences — p. 1, p. 3 and p. 4

No rotation-invariant finitely additive probability measure lives on all subsets of $\mathbb{S}^n$ for $n \ge 2$; no isometry-invariant finitely additive measure on all subsets of $\mathbb{R}^3$ gives the unit ball a finite nonzero value; and an amenable group has no free subgroup of rank two.

Significance

The Banach–Tarski paradox is one of the best-known theorems of twentieth-century mathematics, and it is the reason finitely additive measure theory and amenability exist as subjects. Neither Mathlib nor the platform has it. It has been formalized in Lean outside both: aetilley/banach-tarski, following Tomkowicz and Wagon, proves that the closed unit ball in $\mathbb{R}^3$ is paradoxical under its isometry group, and is a candidate for inclusion in Lean Pool. This mission follows Garrido's statements instead, and publishes each step as a theorem other work can import. Mathlib has the equidecomposition machinery in Equidecomp.lean and the ping-pong lemma, which is the natural tool for Proposition 1.6, but no paradoxical decomposition of anything.

The inclusion $AG \subseteq NF$ completes, with the first Garrido mission's $EG \subseteq AG$, the display $EG \subseteq AG \subseteq NF$ on p. 11 of the notes. Nothing here is a new mathematical result: all of it is classical, and the work is formalization.

Difficulty

Three steps carry the weight. The freeness of $\rho$ and $\sigma$ is a computation the notes defer to Wagon's book: a nonempty reduced word is shown to move a suitable vector, by tracking coordinates of the form $(a, b\sqrt{2}, c)/3^k$ with integers reduced modulo $3$. The absorption of a countable set needs a rotation whose powers move the set off itself, which is a countability argument about angles. And the passage to $\mathbb{S}^n$ for $n > 2$ is only sketched in the notes ("by the same arguments as in Proposition 1.8"): the induction lifts a paradoxical decomposition of $\mathbb{S}^{n-1}$ to $\mathbb{S}^n$ minus two poles, and the poles must then be absorbed by a rotation of $\mathbb{S}^n$.

Transferring the sphere to the ball needs radial projection and the absorption of the center, again by a rotation of infinite order, this time about an axis that misses the center.

Formalization scope

Rotations are matrices: $SO(n+1,\mathbb{R})$ is Matrix.specialOrthogonalGroup (Fin (n + 1)) ℝ, acting on the sphere by mulVec; the bundle proves that an orthogonal matrix preserves the Euclidean norm, so the action is well defined. $E(3)$ is the full group of isometries EuclideanSpace ℝ (Fin 3) ≃ᵢ EuclideanSpace ℝ (Fin 3), as in the first Garrido mission's Corollary 2.5, with an action by evaluation defined in the bundle.

Committed conventions. "Solid ball" is read as a closed ball Metric.closedBall c r with $r > 0$, for every center $c$. "Countable" is Set.Countable, which includes finite sets. Proposition 1.5's second part assumes the set nonempty, since the empty set carries a free action and is not paradoxical. The p. 1 consequence asks for a finite nonzero value on the unit ball: the notes say only "non-zero", and the measure that is $\infty$ on every nonempty set satisfies that. Both departures are named in the statements' descriptions.

One trivialising formalization is ruled out: equidecomposability with the whole group allowed to act on each piece by an arbitrary bijection would make every two sets of the same cardinality equidecomposable. Here each piece is moved by a single group element, through Mathlib's Equidecomp, and paradoxicality needs two disjoint proper subsets.

A complete development needs the sphere and its rotation action, the isometry group of $\mathbb{R}^3$, and the combinatorics of paradoxical decompositions; the definitions are reusable for any later work on the paradox. Contributions are welcome on any milestone. Proposition 1.5 and the step on fixed points of rotations are the most self-contained entry points.

What is left out

The locally compact and measurable versions of the paradox, and the questions of how few pieces suffice, are not in the notes and are not formalized. Tarski's theorem, the converse that a non-paradoxical set carries an invariant measure, is proved in the first Garrido mission and is not restated here.

Selected references

• A. Garrido, An introduction to amenable groups, lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013. archived PDF
• S. Banach and A. Tarski, Sur la décomposition des ensembles de points en parties respectivement congruentes, Fund. Math. 6 (1924), 244–277. DOI
• F. Hausdorff, Bemerkung über den Inhalt von Punktmengen, Math. Ann. 75 (1914), 428–433. DOI
• J. von Neumann, Zur allgemeinen Theorie des Maßes, Fund. Math. 13 (1929), 73–116. DOI
• S. Wagon, The Banach–Tarski Paradox, Cambridge University Press, 1985. DOI