Dynamical Systems

Motivation

The cosmological constant $\Lambda$ entered physics in 1917, when Einstein added a term $\Lambda g_{\mu\nu}$ to his field equations in order to allow a spatially homogeneous universe that neither expands nor contracts (Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, 1917). The resulting Einstein static universe is the unique balance in which the attraction of pressureless matter, the repulsion carried by $\Lambda$, and a positive spatial curvature cancel exactly. Two facts about that balance shaped the next century of cosmology:

1. it is possible only for one specific relation between $\Lambda$, the matter density and the curvature, so the static model is fine-tuned by construction;
2. it is unstable: an arbitrarily small increase of the scale factor grows, and an arbitrarily small decrease collapses.

After Hubble's 1929 observations Einstein dropped the term; it returned in 1998, when the supernova measurements of the Supernova Cosmology Project and the High-$z$ Supernova Search Team required $\Lambda>0$. Interpreting $\Lambda$ as a vacuum energy density $\rho_{\text{vac}}=\Lambda/(8\pi G)$ with equation of state $w=-1$ then produced the cosmological constant problem: the measured value, about $10^{-52}\,\mathrm{m}^{-2}$, is roughly $10^{-122}$ in Planck units, tens of orders of magnitude below the scale that effective quantum field theory suggests (Wikipedia, Cosmological constant problem).

This mission formalizes the classical ordinary-differential-equation content of that story: the static solution, its uniqueness, its instability, the vacuum-energy reading of $\Lambda$, the density-parameter bookkeeping, and the numerical size of the discrepancy.

Setting

A homogeneous isotropic universe is described by a positive scale factor $a:I\to\mathbb{R}$ on a set of times $I\subseteq\mathbb{R}$. Matter is pressureless dust, whose density dilutes with volume,

where $\rho_0>0$ and $a_0>0$ are reference values. Units are geometrized, $c=1$, so $\Lambda$ has dimension (length)$^{-2}$; $G>0$ is Newton's constant and $k\in\mathbb{R}$ the curvature constant.

The dynamics are the two Friedmann equations. The first Friedmann equation is the constraint

and the acceleration equation for dust is

The Hubble parameter is $H=\dot a/a$, the critical density is $\rho_c=3H^2/(8\pi G)$, and the density parameters are

Formalization targets

Goal — the static universe exists for exactly one balance, and it is unstable

For $G,\rho_0,a_0,a_E>0$, the constant function $a\equiv a_E$ satisfies both Friedmann equations if and only if

in which case $\Lambda>0$, $F(a_E)=0$, $F'(a_E)=\Lambda>0$, and the equilibrium is unstable in the following exact sense: every solution of $\ddot a=F(a)$ on $[0,\infty)$ with $a(0)>a_E$ and $\dot a(0)\ge 0$ is strictly increasing and satisfies $a(t)\to\infty$; and every positive solution on $[0,T]$ with $a(0)<a_E$ and $\dot a(0)\le 0$ is strictly decreasing.

Supporting targets

$\Lambda$ is exactly a perfect fluid of constant density $\rho_{\text{vac}}=\Lambda/(8\pi G)$ and pressure $p_{\text{vac}}=-\rho_{\text{vac}}$; the density parameters satisfy $\Omega_m+\Omega_k+\Omega_\Lambda=1$; the acceleration equation is a consequence of the first Friedmann equation along a solution with $\dot a\ne0$; and the observed $\Lambda$ is smaller than $10^{-120}$ in Planck units.

Significance

The static solution is the historical origin of $\Lambda$, and its instability is the reason the static model was never a viable cosmology even before the expansion was observed: the balance point is a local maximum of the effective potential, not a minimum, so the equilibrium cannot be maintained. The same function $F$ and the same linearization $\ddot\delta=\Lambda\,\delta$ govern the late-time behaviour of the standard $\Lambda$CDM model, where the growing mode becomes the de Sitter expansion $e^{\sqrt{\Lambda/3}\,t}$.

What the mission produces on top of the textbook statements: a machine-checked ODE treatment of a dust-plus-$\Lambda$ cosmology that does not stop at the linearized equation. The classical physics argument computes $F'(a_E)=\Lambda$ and calls the equilibrium unstable; the formal statements here ask for the nonlinear conclusion — monotone escape to infinity on one side and strict collapse on the other — which is what "unstable" has to mean for the exact equations. Mathlib contains neither the Friedmann equations nor a general instability criterion for second-order autonomous scalar ODEs, so both have to be built here.

Difficulty

The linearized step is routine calculus. The nonlinear instability is not: from $\ddot a=F(a)$ with $F(a_E)=0$ and $F$ strictly increasing on $(0,\infty)$, one must run a bootstrapping argument in which the sign of $\ddot a$ controls $\dot a$, which in turn controls whether $a$ stays in the region where the sign of $\ddot a$ was known. The obvious approach — solve the ODE explicitly — is not available: the dust-plus-$\Lambda$ equation with the static value of $k$ has no elementary closed-form solution through the static point, and the first Friedmann equation, which is the conserved energy of the second, degenerates exactly at $a=a_E$, where $\dot a=0$. Divergence $a(t)\to\infty$ additionally requires ruling out that $\dot a$ stalls, i.e. a quantitative lower bound on $\dot a$ once the solution has left a neighbourhood of $a_E$.

Formalization scope

Everything is stated for real-valued functions $a:\mathbb{R}\to\mathbb{R}$ of a real time variable; derivatives are the usual derivative of a real function, and each equation is asserted pointwise on an explicit set of times ($\mathbb{R}$, $[0,\infty)$, $[0,T]$, or a general open set), never globally by fiat. Dust density, the Friedmann equations, the acceleration function $F$, the Hubble parameter, the critical density and the three density parameters are all fixed in one definition file shared by every statement, so all items commit to the same conventions: $c=1$, curvature entering as $-k$ in the equation for $\dot a^2$, and $\rho_0,a_0$ as fixed reference constants rather than the value of the density at a particular time.

Two trivializing readings are ruled out explicitly. First, the contracting-side statement is posed on a bounded interval $[0,T]$ with positivity of $a$ assumed there, because a collapsing solution reaches $a=0$ in finite time; posing it on $[0,\infty)$ would make its hypotheses unsatisfiable and the statement vacuous. Second, the escape statement asks for $a(t)\to\infty$, not merely $\dot a\ge0$, so it cannot be satisfied by a solution that converges to a finite limit.

Useful contributions beyond the listed items: a reusable instability criterion for $\ddot x=F(x)$ at a zero of $F$ with $F'>0$, and the corresponding stability criterion, both of which are independent of cosmology.

Selected references

• Wikipedia, Cosmological constant. https://en.wikipedia.org/wiki/Cosmological_constant
• Wikipedia, Cosmological constant problem. https://en.wikipedia.org/wiki/Cosmological_constant_problem
• A. Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 1917.
• S. Weinberg, The cosmological constant problem, Reviews of Modern Physics 61 (1989) 1. https://doi.org/10.1103/RevModPhys.61.1
• J. Martin, Everything you always wanted to know about the cosmological constant problem (but were afraid to ask), Comptes Rendus Physique 13 (2012) 566. https://doi.org/10.1016/j.crhy.2012.04.008

Motivation

A coupling constant is the number that fixes the strength of an interaction: it is the coefficient that multiplies the interaction term of a Lagrangian relative to its kinetic term, and in a perturbative treatment it is the parameter the expansion is organised in. The central structural fact about such a coupling in a quantum field theory is that it is not constant: once quantum corrections are resummed, the coupling depends on the energy scale $\mu$ at which the theory is probed. This scale dependence — the running of the coupling — is what distinguishes quantum electrodynamics, whose coupling grows with energy until perturbation theory breaks down (the Landau pole), from quantum chromodynamics, whose coupling decreases logarithmically at high energy (asymptotic freedom, Gross–Politzer–Wilczek, Nobel Prize in Physics 2004).

This mission formalizes the elementary mathematics behind those statements: the one-loop renormalization-group equation, its exact solution, and the two qualitatively different behaviours it produces depending on the sign of the one-loop coefficient. The source is the Wikipedia article Coupling constant (sections Beta functions, QED and the Landau pole, QCD and asymptotic freedom), which states these facts in prose and in the single displayed formula for the running QCD coupling.

Setting

Write $g$ for a single real coupling and $t = \log \mu$ for the logarithm of the energy scale. The beta function is defined by

and at one loop $\beta$ is a cubic monomial,

with a scheme- and theory-dependent real coefficient $b$. Saying that $g$ runs at one loop on a set of scales $S$ means that $g$ is differentiable at every $t \in S$ with $g'(t) = b\,g(t)^{3}$.

For QCD the article records the one-loop form of the strong coupling directly in terms of the process energy $Q$ and the QCD scale $\Lambda$:

Target

The goal theorem is the dichotomy governed by the sign of $b$, for an initial condition $g(0) = g_0 > 0$ at the reference scale $t = 0$:

1. Asymptotic freedom ($b < 0$). Every solution on $[0,\infty)$ satisfies

i.e. $g(t)^{2} \sim 1/(2|b|\log\mu)$: the coupling dies off logarithmically in the energy.

2. Landau pole ($b > 0$). No solution exists on the whole closed interval

the flow cannot be continued up to the finite scale $t_\ast = 1/(2bg_0^{2})$, which is the Landau pole of the one-loop approximation.

Both follow from the exact one-loop solution, which is itself a milestone:

Significance

The dichotomy above is the mathematical content of the two headline claims made about running couplings: that a positive one-loop coefficient drives the coupling to infinity at a finite energy, and that a negative one makes it vanish logarithmically at high energy. The milestones also isolate the statement that a vanishing beta function means the coupling does not run at all (scale invariance), and record the elementary analytic properties of the explicit QCD formula $\alpha(Q) = 1/(\beta_0\log(Q^2/\Lambda^2))$: it is strictly decreasing above $\Lambda$, tends to $0$ as $Q\to\infty$, and satisfies the one-loop flow equation $d\alpha/dQ = -(2/Q)\,\beta_0\,\alpha^{2}$.

Nothing here is open mathematics: these are exercises in the theory of a separable scalar ODE. What the mission produces is a machine-checked, reusable Lean development of the one-loop renormalization-group flow — a small piece of formalized physics infrastructure that later missions on renormalization or dimensional transmutation can import.

Difficulty

The only real subtlety is that the exact solution is obtained by differentiating $t \mapsto g(t)^{-2}$, which requires knowing in advance that the solution never vanishes. Positivity is not assumed: it is a separate milestone, and must be derived from the initial condition together with the flow equation (if $g$ reached $0$ at a first time $t_1$, the identity $g(t)^{-2} = g_0^{-2} - 2bt$ on $[0,t_1)$ forces $g(t_1)^2$ to have a strictly positive limit). The Landau-pole statement is a non-existence claim and has no analytic content beyond this, but it does depend on the positivity step.

Formalization scope

Scales are parametrised logarithmically: the independent variable is $t = \log\mu \in \mathbb{R}$, the coupling is a function $g : \mathbb{R} \to \mathbb{R}$, and the flow hypothesis is imposed pointwise as a two-sided derivative at each point of the given set (at an endpoint of a closed interval this is slightly stronger than a one-sided derivative, which only strengthens the hypotheses of the positive results and weakens the non-existence claim — the Landau pole statement is therefore the conservative reading). No uniqueness or existence theory for ODEs is assumed; the statements quantify over arbitrary functions satisfying the flow equation. The QCD formula is taken with real arguments and no constraint tying $\beta_0$ or $\Lambda$ to a particular number of flavours; the numerical values quoted in the source ($\alpha_s(M_Z^2) = 0.1179 \pm 0.0010$, $\Lambda \approx 332$ MeV) are measurements and are deliberately not formalized.

Degenerate cases are visible in the statements rather than hidden: $b = 0$ appears as its own milestone (constant coupling), and the value of $\alpha(Q)$ for $Q \le \Lambda$, where the logarithm is non-positive or zero, is never asserted.

Selected references

• Coupling constant, Wikipedia, revision 1354339557, https://en.wikipedia.org/w/index.php?title=Coupling_constant&oldid=1354339557
• A. Deur, S. J. Brodsky, G. F. de Téramond, "The QCD running coupling", Progress in Particle and Nuclear Physics 90 (2016) 1–74, https://arxiv.org/abs/1604.08082
• Particle Data Group (P. A. Zyla et al.), "Review of Particle Physics — Quantum Chromodynamics", PTEP 2020 (8), https://doi.org/10.1093/ptep/ptaa104

Motivation

Roughly half of the stars in our galaxy belong to binary star systems: pairs of stars close enough to each other that their mutual gravitational attraction dominates every other influence, and far enough from every other star that the rest of the galaxy can be ignored. Such a pair is the cleanest physical realization of the Newtonian two-body problem, and it is the reason the two-body problem is not merely a textbook exercise: the masses of stars other than the Sun are known almost entirely because binaries can be observed, and the observation is converted into a mass by exactly the chain of reasoning formalized in this mission.

This mission formalizes Section 4.16, "Binary star systems", of Richard Fitzpatrick's Celestial Mechanics lecture notes (University of Texas at Austin), Eqs. (4.108)–(4.119). It is the first mission of a planned series on the same source; the whole series shares the Lean namespace CelestialMechanics.

Setting

Two point masses $m_1, m_2 > 0$ move in $\mathbb{R}^3$ under Newtonian gravity, with position vectors $\mathbf{r}_1(t)$ and $\mathbf{r}_2(t)$ defined for all times $t \in \mathbb{R}$. Write $\mathbf{r} = \mathbf{r}_2 - \mathbf{r}_1$ for the relative separation and $r = \lVert \mathbf{r} \rVert$ for the distance between the stars. The gravitational force the first star exerts on the second is Eq. (4.108),

and Newton's second law for each star reads

A pair of twice continuously differentiable, never-colliding trajectories satisfying these two equations is what this mission calls a Newtonian gravitational two-body system.

Three derived objects organize the material. The center of mass is $\mathbf{R} = (m_1\mathbf{r}_1 + m_2\mathbf{r}_2)/(m_1+m_2)$. The relative Kepler problem with gravitational parameter $GM$, $M = m_1+m_2$, is the equation

for a nowhere-vanishing curve $\mathbf{r}$. A Keplerian conic orbit with major radius $a$, eccentricity $e$ and angular momentum per unit reduced mass $h$ is a planar curve given in polar coordinates $(\rho, \theta)$ by

which are Eqs. (4.112)–(4.114); the elements are tied together by Eq. (4.115), $a = h^{2}/\bigl((1-e^{2})GM\bigr)$.

Target

The goal theorem is an existence-and-description statement: for every $G>0$, every pair of masses $m_1,m_2>0$ and every choice of orbital elements $a>0$, $0 \le e < 1$, there exist trajectories $\mathbf{r}_1, \mathbf{r}_2$, polar functions $\rho, \theta$ and a time $T>0$ such that

The milestones are the individual steps of Section 4.16, ordered as in the source: the reduction of the two-body system to the one-body problem (4.110)–(4.111); the uniform motion of the center of mass, which makes the center-of-mass frame inertial; the positions of the two stars in that frame (4.118)–(4.119); the verification that the conic (4.112)–(4.115) solves (4.110); the period of revolution (4.116)–(4.117); and the inversion of these relations that yields the two stellar masses from observation.

Significance

The result itself. The theorem is the complete qualitative and quantitative picture of a binary orbit: each star traverses an ellipse about the common center of mass, the two stars are diametrically opposite one another at every instant, the distances from the center of mass are in the fixed ratio $m_2 : m_1$, and the period depends only on the major radius and the total mass. The last two facts are what astronomers use: the measured pair $(a, T)$ gives the mass sum $m_1 + m_2 = 4\pi^{2}a^{3}/(GT^{2})$, the observed ratio of the two apparent orbits gives $m_1/m_2$, and sum plus ratio give the individual masses. The same reduction also supplies the finite-mass correction to one-body solar-system orbit theory, in which $G M_{\odot}$ is replaced by $G(M_{\odot} + m)$.

Formalizing it. The mathematics has been settled since Newton, so the contribution here is a machine-checked development rather than a new result. Mathlib currently has extensive analysis infrastructure — iterated derivatives, ContDiff, Euclidean spaces — but no development of the Kepler problem: neither the conic solution of the inverse-square equation of motion nor Kepler's laws. The reusable output of this mission is therefore a small, self-contained Kepler library: the two-body reduction, the conic solution, and the period law, stated for curves in $\mathbb{R}^3$ in a form that later missions in the series (perturbations, orbital elements, the restricted three-body problem) can import unchanged.

Difficulty

Two milestones carry essentially all of the analytic work.

The first is showing that the conic really solves (4.110). The obvious route — differentiate $\rho(t)$ twice and simplify — runs into the fact that $\rho$ is given as a function of $\theta(t)$ and $\theta$ is given only implicitly, through the angular-momentum law $\dot\theta = h/\rho^{2}$. Even the regularity in the conclusion has to be earned: the hypotheses supply only differentiability of $\theta$, and twice-continuous differentiability of the curve must be bootstrapped from the two polar equations. Getting the Cartesian second derivative into the form $-(GM/\rho^{3})\mathbf{r}$ requires the relation $h^{2} = (1-e^{2})GMa$ at exactly the right place, and this is where a sign or a factor typically goes wrong.

The second is the goal theorem, which is an existence statement and therefore needs the angular equation $\dot\theta = h/\rho(\theta)^{2}$ to be solved globally in time, on all of $\mathbb{R}$ and not merely on a small interval. The right-hand side is smooth and, for $0 \le e < 1$, bounded above and below by positive constants, so the solution exists for all time and advances by $2\pi$ in a fixed time $T$; but "exists for all time" is a real obligation in Lean, and a naive appeal to a local existence theorem does not discharge it.

Formalization scope

Space is EuclideanSpace ℝ (Fin 3), so the norm is the Euclidean one and the three Cartesian components are indexed $0, 1, 2$; the orbital plane is fixed to be the $x$-$y$ plane, exactly as in Eq. (4.112). Trajectories are total functions $\mathbb{R} \to \mathbb{R}^3$: all statements are global in time, and no restriction to an interval or to positive times is made. Derivatives are iteratedDeriv, and smoothness is ContDiff ℝ 2. Masses and $G$ are positive reals wherever the physics needs it, and this is stated explicitly rather than left implicit. Eccentricity is restricted to $0 \le e < 1$ throughout, so only bound (elliptical and circular) orbits are in scope; the parabolic and hyperbolic cases of Sections 4.13–4.15 are left to later missions.

Two trivializing formalizations are ruled out by construction. The definitions never allow the separation to vanish, so no statement is satisfied by a collision; and in the goal theorem the angular momentum $h$ and the period $T$ are not existentially quantified but pinned to their Keplerian values in terms of $(G, m_1+m_2, a, e)$, so the orbit cannot be rescaled to make the conditions easy to meet.

Contributions of independent interest are welcome: conservation of angular momentum and of energy for (4.110), the equal-areas law, the eccentricity (Laplace–Runge–Lenz) vector, and the Kepler equation relating mean and eccentric anomaly all sit naturally on top of this development.

Selected references

• Richard Fitzpatrick, Celestial Mechanics, University of Texas at Austin lecture notes, Chapter 4 "Keplerian orbits", Section 4.16 "Binary star systems", https://farside.ph.utexas.edu/teaching/celestial/Celestial/node38.html. The source of this mission; Eqs. (4.108)–(4.119).
• Isaac Newton, Philosophiæ Naturalis Principia Mathematica, 1687. Book I contains the original solution of the inverse-square two-body problem.

Motivation

In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is remarkable both for how little it assumes — continuity, nothing more — and for how much it concludes: the set of periods of the periodic orbits of such a map is completely constrained by a single linear ordering of the positive integers. Its best-known corollary, rediscovered by Li and Yorke in 1975 under the slogan period three implies chaos, says that a continuous map of $\mathbb{R}$ with an orbit of period three has orbits of every period.

Devaney presents the theorem in §1.10 of An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering relations. This mission is the second in a series formalizing the book; it is independent of the first, sharing only the book-wide namespace.

Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave the short interval-covering proofs, the latter being the one Devaney reproduces.

Setting

Let $f : \mathbb{R} \to \mathbb{R}$ be continuous. A point $x$ has prime period $n \ge 1$ if $f^{n}(x) = x$ and $f^{m}(x) \ne x$ for every $0 < m < n$.

The Sarkovskii ordering of the positive integers is

first the odd numbers greater than one in increasing order, then $2$ times the odds, then $2^2$ times the odds, and so on; the powers of two come last, in decreasing order. Writing $k = 2^{a}p$ and $\ell = 2^{b}q$ with $p, q$ odd, $k \triangleright \ell$ holds exactly when either $p, q > 1$ and $(a,p)$ precedes $(b,q)$ lexicographically, or $p > 1$ and $q = 1$, or $p = q = 1$ and $b < a$.

Two elementary facts drive the proof. If $I$ is a closed interval with $f(I) \supseteq I$, then $f$ has a fixed point in $I$; and if closed intervals satisfy $f(A_i) \supseteq A_{i+1}$ for $i < n$, then some point of $A_0$ has $f^{i}(x) \in A_i$ for all $i \le n$. One writes $I \to J$, "$f(I)$ covers $J$", for $J \subseteq f(I)$.

Target

The goal is Devaney's Theorem 10.2: for continuous $f : \mathbb{R} \to \mathbb{R}$,

The milestones are the steps of the book's proof: the two covering observations, the period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed case $p \cdot 2^m$ into which the general theorem is decomposed, the remark that a period which is not a power of two forces infinitely many periodic points, and the converse direction, witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.

Significance

Sarkovskii's theorem is the sharpest general statement known about the period structure of one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no stronger implication holds. Its first consequence — only powers of two can occur as the set of periods of a map with finitely many periodic points — is what makes the period-doubling cascade the canonical route to chaos, a theme the book returns to in §1.17.

The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by $120^\circ$ has every point of period three and no other period.

Formalizing it contributes a reusable Lean treatment of interval covering relations and of the Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and the covering machinery is exactly what §1.13 and §1.16 of the book reuse.

Difficulty

The period-three case is a short argument once the covering observations are available, and it is a reasonable first milestone. The general theorem is not: the odd case requires choosing the right interval $I_1 = [x_i, x_{i+1}]$ on the orbit, building the increasing family of unions $O_\ell$ of covered intervals, and showing that the shortest return loop has length exactly $n-1$ — a combinatorial argument on the cyclic order of the orbit that is easy to draw and tedious to formalize. Attempts to shortcut the ordering with a naive induction on $n$ fail: the statement for $n$ genuinely depends on the geometric arrangement of the orbit points.

Formalization scope

1. Periodicity is prime period throughout: $f^n(x) = x$ together with minimality of $n$. The statements would be false or trivial with "period" read as "fixed by $f^n$".
2. The Sarkovskii relation is defined arithmetically, in terms of the $2$-adic valuation and the odd part of an integer, rather than as a listed order; it is a strict relation, so $k \triangleright k$ is false and the goal theorem says nothing about $\ell = k$ (which holds by hypothesis anyway).
3. $0$ is outside the ordering: the relation is false whenever either argument is $0$.
4. Intervals in the covering lemmas are closed intervals $[a,b]$ with $a \le b$, given by their endpoints; "covers" means containment of the interval in the image, $J \subseteq f(I)$.
5. The converse milestone asserts the existence of a continuous map with a period-five point and no period-three point; the book's witness is piecewise linear on $[1,5]$, but the statement does not prescribe it.

Selected references

• Robert L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd edition, Westview Press, 2003 (ISBN 0-8133-4085-3) — §1.10, pp. 60–68. The mission's primary source.
• T. Y. Li and J. A. Yorke, Period three implies chaos, American Mathematical Monthly 82 (1975), 985–992, DOI: 10.1080/00029890.1975.11994008.
• L. Block, J. Guckenheimer, M. Misiurewicz, L. S. Young, Periodic points and topological entropy of one-dimensional maps, in Global Theory of Dynamical Systems, Lecture Notes in Mathematics 819, Springer, 1980, 18–34, DOI: 10.1007/BFb0086977 — the proof Devaney follows.

Audit note (provenance of the read-backs)

The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.

Every definition and statement in this proposal was compiled locally against this mission's environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files elaborate with no errors, the only warnings being the expected sorry placeholders in the theorem bodies.

Motivation

The word chaos entered mathematics with a precise meaning, and Robert L. Devaney's An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003) is the text that fixed the meaning now used in most of the literature: a map is chaotic when it is unpredictable (sensitive dependence on initial conditions), indecomposable (topological transitivity), and nevertheless regular (dense periodic points). The book develops this definition on the simplest possible object — the real quadratic family $F_\mu(x) = \mu x(1-x)$ on the unit interval — and shows that for large $\mu$ the map is chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.

This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8: the invariant set of the quadratic family, symbolic dynamics on the sequence space $\Sigma_2$, topological conjugacy, and Devaney's definition of chaos. Everything later in the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets — is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the vocabulary of the whole series.

Setting

Write $I = [0,1]$ and let $F_\mu(x) = \mu x(1-x)$ for a real parameter $\mu$. Iterates are written $F_\mu^n$, with $F_\mu^0$ the identity.

For $\mu > 4$ the maximum value $\mu/4$ of $F_\mu$ exceeds $1$, so some points of $I$ leave $I$ after one iteration. Let

so that $A_n$ is the set of points escaping from $I$ at the $(n+1)$-st iteration. The set of points that never escape is

The complement $I \setminus A_0$ consists of two closed intervals, $I_0$ to the left of the midpoint $1/2$ and $I_1$ to its right.

On the symbolic side, $\Sigma_2$ is the set of one-sided infinite sequences $s = (s_0 s_1 s_2 \dots)$ with $s_i \in \{0,1\}$, metrized by

and $\sigma : \Sigma_2 \to \Sigma_2$ is the shift map $\sigma(s_0 s_1 s_2 \dots) = (s_1 s_2 s_3 \dots)$. The itinerary of $x \in \Lambda$ is the sequence $S(x) = (s_0 s_1 s_2 \dots)$ with $s_j = 0$ when $F_\mu^{\,j}(x) \in I_0$ and $s_j = 1$ when $F_\mu^{\,j}(x) \in I_1$.

Following Devaney, $f : J \to J$ is topologically transitive if for every pair of open sets $U, V$ meeting $J$ there is $k > 0$ with $f^k(U \cap J) \cap V \neq \emptyset$; it has sensitive dependence on initial conditions if there is $\delta > 0$ such that every point of $J$ has points of $J$ arbitrarily near it whose orbit eventually separates from its own by more than $\delta$; and it is chaotic on $J$ when it has sensitive dependence, is topologically transitive, and has a dense set of periodic points in $J$.

Target

The goal is Devaney's Example 8.8: for $\mu > 2 + \sqrt 5$,

The milestones are the results the book uses to get there, in the book's own order: the escape of orbits outside $I$ (Proposition 5.2), the tame regime $1 < \mu < 3$ (Proposition 5.3), the Cantor structure of $\Lambda$ (Theorem 5.6), the metric and dynamics of the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of $F_4$ on all of $I$ (Example 8.9).

Significance

The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic by producing a conjugacy with a shift. The conjugacy also gives quantitative information that is otherwise inaccessible — for example, that $F_\mu$ has exactly $2^n$ points fixed by $F_\mu^{\,n}$, which no direct computation with the degree-$2^n$ polynomial delivers.

Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's three chaos conditions, the sequence space $\Sigma_2$ with its metric and shift, topological conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the foundation the rest of the book's series will import.

Difficulty

The obvious route to the goal — analyze $F_\mu$ on $\Lambda$ directly — fails, because $\Lambda$ has no explicit description: it is a nested intersection of $2^{n+1}$ intervals whose endpoints are not available in closed form. The whole argument therefore goes through the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which needs the nested-interval construction $I_{s_0 \dots s_n} = I_{s_0} \cap F_\mu^{-1}(I_{s_1}) \cap \dots \cap F_\mu^{-n}(I_{s_n})$ together with the fact that these intervals are nonempty and nested; and (ii) injectivity, which needs the hyperbolicity estimate $|F_\mu'| > \lambda > 1$ on $I_0 \cup I_1$, valid exactly because $\mu > 2 + \sqrt 5$, and the mean value theorem. The hypothesis $\mu > 2 + \sqrt 5$ is not cosmetic: Devaney notes the results hold for $\mu > 4$, but only with a more delicate argument.

Formalization scope

The Lean development fixes the following conventions.

1. $\Lambda$ is defined as $\{x : \forall n,\ F_\mu^{\,n}(x) \in [0,1]\}$ — the points whose whole forward orbit stays in $I$ — rather than as a complement of the sets $A_n$; the two descriptions agree, and the definitional form makes invariance immediate. The sets $A_0, A_n, I_0, I_1$ are nonetheless defined, since the book's arguments refer to them.
2. The itinerary is defined as a total function of a real argument, taking entry $0$ at step $n$ when $F_\mu^{\,n}(x) \le 1/2$ and $1$ otherwise. On $\Lambda$ this agrees with Devaney's $I_0/I_1$ test, since the midpoint $1/2$ lies in the gap $A_0$ when $\mu > 4$.
3. $\Sigma_2$ carries Devaney's metric $d$ literally, as a summable series, not merely a topology; the metric space instance is part of the definitional layer, so Proposition 6.2 is not a separate milestone.
4. Sensitive dependence, transitivity, chaos and periodicity are stated for a map $f : X \to X$ of a metric space together with an invariant subset $J$, using open sets of the ambient space intersected with $J$; this avoids subtype bookkeeping while keeping the relative formulation of the book.
5. Cardinality claims ("$\operatorname{Per}_n$ has $2^n$ elements") are stated with Set.ncard and are restricted to $n > 0$; for $n = 0$ every point is fixed by $F^0$ and the claim would be false.
6. Nothing here is vacuous: the hypothesis $\mu > 2+\sqrt 5$ is satisfiable, $\Lambda$ is nonempty (it contains $0$), and the chaos predicate is a conjunction of three nontrivial conditions rather than a definitional abbreviation.

Contributions of any kind are welcome: full proofs, reductions splitting a milestone into lemmas, and reusable lemmas about $\Sigma_2$ or about conjugacy that later missions in the series can import.

Selected references

• Robert L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd edition, Westview Press, 2003 (ISBN 0-8133-4085-3) — §1.5 (pp. 31–38), §1.6 (pp. 39–43), §1.7 (pp. 44–47), §1.8 (pp. 49–52). The mission's primary and authoritative source.
• J. Banks, J. Brooks, G. Cairns, G. Davis, P. Stacey, On Devaney's definition of chaos, American Mathematical Monthly 99 (1992), 332–334, DOI: 10.1080/00029890.1992.11995856 — proves that transitivity plus dense periodic points already imply sensitive dependence.

Audit note (provenance of the read-backs)

The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.

Every definition and statement in this proposal was compiled locally against this mission's environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files elaborate with no errors, the only warnings being the expected sorry placeholders in the theorem bodies.

Motivation

The Riemann hypothesis asserts that every non-trivial zero of the Riemann zeta function $\zeta$ lies on the line $\operatorname{Re} s = 1/2$; the simplicity hypothesis asserts in addition that every such zero is a simple zero of $\zeta$. Both are statements about the location and the order of a discrete set of points in the complex plane, and almost every reformulation of them stays inside analytic number theory.

Kawahira (2016) gives a reformulation of a different kind. He attaches to $\zeta$ an explicit meromorphic self-map of the Riemann sphere and shows that the Riemann hypothesis together with the simplicity hypothesis is equivalent to a statement about the local dynamics of that map: it has no attracting fixed point. The translation is elementary once the right object is in place — the holomorphic index (residue fixed point index) of a fixed point — and it turns a question about zeros into a question about stability. This mission formalizes that translation, together with the supporting propositions on indices and multipliers that make it work.

Setting

For a non-constant meromorphic $g : \mathbb{C} \to \widehat{\mathbb{C}}$, define the nu function

If $\alpha \neq 0$ is a zero of $g$ of order $m \ge 1$, then $\alpha$ is a fixed point of $\nu_g$ with multiplier

and if $\alpha$ is a pole of order $m$ the multiplier is $1 + \frac{1}{m\alpha}$. A fixed point $\alpha$ of a holomorphic map $f$ is attracting if $|f'(\alpha)| < 1$, indifferent if $|f'(\alpha)| = 1$, and repelling if $|f'(\alpha)| > 1$.

The holomorphic index of $f$ at a fixed point $\alpha$ is

the integral being over a small positively oriented circle around $\alpha$. When the multiplier $\lambda$ is not $1$ one has $\iota = \frac{1}{1-\lambda}$, and the Möbius map $\lambda \mapsto \frac{1}{1-\lambda}$ carries the unit disk onto the half-plane $\operatorname{Re}\iota > 1/2$. So a fixed point is attracting, indifferent or repelling exactly according to whether $\operatorname{Re}\iota$ is $> 1/2$, $= 1/2$ or $< 1/2$: the critical line reappears, in the index plane.

The point of the construction is that $\nu_g$ is engineered so that the index of $\nu_g$ at a simple zero $\alpha$ of $g$ is $\alpha$ itself (and $m\alpha$ at a zero of order $m$). Writing $\nu_\zeta = \nu_g$ for $g = \zeta$: a non-trivial zero $\alpha$ of order $m$ has index $m\alpha$, so $\operatorname{Re}\iota = m\operatorname{Re}\alpha$, and asking that this equal $1/2$ is asking for $m = 1$ and $\operatorname{Re}\alpha = 1/2$.

Formalization targets

Goal — Theorem 1 of the paper, conditions (a), (b), (c)

Supporting targets

The milestones are the paper's Propositions 3, 4, 5, 7, 8, 9, its Theorem 11 (the variant for the Riemann xi function $\xi$), and Proposition 13 of the appendix (the Newton map $N_g(z) = z - g(z)/g'(z)$, for which every zero of $g$ becomes an attracting fixed point — the contrast that explains why $\nu_g$, and not $N_g$, sees the critical line).

Significance

The equivalence converts the simultaneous truth of the Riemann and simplicity hypotheses into the non-existence of an attracting fixed point of one explicitly given meromorphic function. Nothing in the translation is conjectural: the content is the index computation, the symmetry $\alpha \mapsto 1 - \alpha$ of the non-trivial zeros supplied by the functional equation, and the classification of fixed points by the real part of the index. What a formalization adds is a machine-checked statement of the dictionary, and a reusable Lean development of the holomorphic index, which Mathlib does not currently contain — the index, its relation to the multiplier, and its behaviour at zeros and poles are general facts of one-variable complex dynamics, independent of this application.

Status, precisely: the Riemann hypothesis is open, and this mission does not ask anyone to settle it. Every target here is a theorem with a published proof; the work is to formalize those proofs. The goal theorem is an equivalence between two open statements, so it is provable without deciding either side.

Difficulty

The obvious route to the goal — compute $\nu_\zeta'$ at a zero, apply the classification, done — fails in one direction. From "no attracting fixed point" one gets $\operatorname{Re}(m\alpha) \le 1/2$ for each non-trivial zero $\alpha$ of order $m$, which alone excludes neither a multiple zero nor a zero to the left of the critical line. The functional equation must be used to pair $\alpha$ with $1-\alpha$, whose index is $m(1-\alpha)$; only the two inequalities together force $m = 1$ and $\operatorname{Re}\alpha = 1/2$. A complete Lean proof therefore needs, besides the local computation: that the non-trivial zeros lie in the open strip $0 < \operatorname{Re} s < 1$, that $\alpha$ and $1-\alpha$ are zeros of the same order, and that the trivial zeros and the pole at $s = 1$ give repelling fixed points.

The index milestone (Proposition 3) is a residue computation on a small circle, and the hypotheses have to be arranged so that $z - f(z)$ has exactly one zero inside; the other genuinely analytic milestone is the order-$m$ computation of $\nu_g'$, where $g'$ vanishes at the fixed point when $m \ge 2$ and the singularity is removable rather than absent.

Formalization scope

The development is over $\mathbb{C}$ with Mathlib's riemannZeta. Conventions the Lean statements commit to:

1. Non-trivial zero means: a zero of $\zeta$ that is not one of $-2, -4, -6, \dots$. Nothing about the critical strip is built into the definition; that the non-trivial zeros lie in $0 < \operatorname{Re} s < 1$ is part of the work.
2. Simplicity of a zero $\alpha$ is expressed as $\zeta'(\alpha) \neq 0$.
3. $\nu_g$ is a total function $\mathbb{C} \to \mathbb{C}$, using Lean's convention that division by zero returns zero. At a zero of $g$ this total function agrees with the genuine holomorphic extension of $\nu_g$, so multipliers there are the true ones. At a point where $g$ is non-zero and $g'$ vanishes, and at a pole of $g$, the total function takes an artefactual value; the statements about $\nu_\zeta$ therefore carry the explicit guard $\zeta(\alpha) = 0 \vee \zeta'(\alpha) \neq 0$ together with $\alpha \neq 0, 1$. The excluded points are exactly the pole of $\zeta$ (a repelling fixed point, by Proposition 7 of the paper) and the poles of $\nu_\zeta$, so the guarded statements are equivalent to the paper's, but they are guarded, and a reader should check that they consider the guards faithful.
4. The xi function is taken in Kawahira's normalization $\xi(z) = \frac{1}{2}z(1-z)\pi^{-z/2}\Gamma(z/2)\zeta(z)$, written in Lean through Mathlib's entire function $\Lambda_0$ so that the Lean $\xi$ is entire and has the correct values at $z = 0, 1$ rather than removable-singularity artefacts; the definition file carries a proved lemma identifying it with $\frac{1}{2}z(1-z)\Lambda(z)$ off $\{0,1\}$.
5. Conditions (d) and (e) of the paper's Theorems 1 and 10 — the purely topological reformulations in terms of a topological disk $D$ with $\nu_\zeta(D) \subset D$, and their homeomorphic deformations — are not part of this mission. They rest on the topological characterization of attracting fixed points (the paper's Proposition 2), whose proof uses the Riemann mapping theorem and the Schwarz–Pick lemma; the Riemann mapping theorem is not available in Mathlib, and the intended strength of the inclusion $\nu_\zeta(D) \subset D$ (compact containment) needs to be fixed before the statement can be formalized faithfully. Theorem 14 of the appendix, which is of the same topological kind, is likewise out of scope. A contribution supplying Proposition 2 in a defensible form would be welcome, as a separate mission.

Nothing here is vacuous: the goal is an equivalence of two statements each of which is satisfiable in form, and the guards exclude only points at which the Lean encoding of $\nu_\zeta$ is known not to model the meromorphic map.

Reusable beyond this mission: the holomorphic index, the multiplier classification, the general nu-function and Newton-map computations at a zero of order $m$ — all stated for an arbitrary function analytic at the point, not for $\zeta$.

Selected references

• T. Kawahira, The Riemann Hypothesis and Holomorphic Index in Complex Dynamics, Experimental Mathematics (2016). https://doi.org/10.1080/10586458.2016.1217443
• J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. (Holomorphic index: Lemma 12.2; topological characterization of fixed points: Section 8.)
• E. C. Titchmarsh, The Theory of the Riemann Zeta Function, 2nd ed., Oxford University Press, 1986. (Functional equation; trivial zeros; the xi function.)
• D. Schleicher, Newton's Method as a Dynamical System: Efficient Root Finding of Polynomials and the Riemann $\zeta$ Function, Fields Inst. Commun. 53 (2008), 213–224.

Motivation

Von Neumann introduced amenability in 1929 in response to the Banach–Tarski paradox: a group is amenable when it carries a finitely additive, translation-invariant probability measure on its subsets, and no amenable group contains a free subgroup of rank $2$ — which is exactly what the paradox needs. The converse is the von Neumann conjecture, and it is false: Ol'shanskii in 1980 and Adyan in 1982 produced finitely generated counterexamples. A finitely presented counterexample was harder, and one candidate stood out — Richard Thompson's group $F$, finitely presented, with nobody able to decide whether it was amenable.

Brin and Squier attacked it and in 1985 got what they called "half a success": they proved that $F$, and more generally the group $\mathrm{PLF}(\mathbb{R})$ of piecewise-linear homeomorphisms of the line with finitely many breakpoints, contains no free subgroup of rank greater than $1$. Whether $F$ is amenable they could not determine, and it is still open today; claimed proofs have appeared in both directions and none has been accepted. Finitely presented counterexamples were eventually found by other routes (Ol'shanskii–Sapir 2002; Lodha–Moore 2016), so $F$ is no longer needed as a candidate. This mission formalizes the half that was settled.

Setting

Let $\mathrm{Homeo}_+(\mathbb{R})$ be the group of orientation-preserving homeomorphisms of the line: the strictly increasing bijections $\mathbb{R}\to\mathbb{R}$ under composition. The support of $f$ is the set of points it moves, $\operatorname{supp} f = \{\,t : f(t)\neq t\,\}$, an open subset of $\mathbb{R}$.

A continuous $f$ is piecewise linear when there is a discrete set $B$ of breakpoints with $f$ differentiable off $B$ and $f'$ constant on each component of $\mathbb{R}\setminus B$; for finite $B$ this is the same as $f$ being affine on a neighbourhood of every point outside $B$. Nothing is required at the points of $B$, so the two affine pieces meeting at a breakpoint may disagree — that is what makes such an $f$ more than an affine map. Write $\mathrm{PL}(\mathbb{R})$ for the piecewise-linear elements of $\mathrm{Homeo}_+(\mathbb{R})$ and

for the subgroup this mission is about. The distinction matters: the goal below holds in $\mathrm{PLF}(\mathbb{R})$ and fails in $\mathrm{PL}(\mathbb{R})$, where Brin and Squier build free subgroups of rank $2$ by lifting them from the circle. Write $\mathrm{PLF}'(\mathbb{R})$ for the commutator subgroup, which Brin and Squier identify as the elements whose slope at each end is $1$ — an element has slope $a$ at an end when it agrees with a single affine map of slope $a$ on a ray out to that end. Thompson's group $F$ — the piecewise-linear homeomorphisms of $[0,1]$ with dyadic breakpoints and power-of-two slopes — is realized inside $\mathrm{PLF}(\mathbb{R})$.

Formalization targets

Goal — no two elements generate freely

Since a free group of rank greater than $1$ contains one of rank $2$, this is Brin and Squier's Theorem (3.1).

The dichotomy it rests on

Their Theorem (3.2), with the conclusion weakened to what the goal consumes. What they prove is infinite rank, which needs the general form of their Lemma (1.2); that general Lemma and the full-strength (3.2) are milestones of their own here. The goal itself only ever uses the rank-two form.

The twenty-four milestones

Thirteen are numbered results of theirs: the support observations (1.1a), (1.1b); Lemma (1.2) in its rank-two case and in its general form; Lemmas (3.4) and (3.5), already formalized and published, entering as references; the commutator facts (2.14a), (2.14b), (2.14c); Theorem (3.2) both as the rank-two dichotomy the goal consumes and at full strength; and Corollary (3.3), likewise in both strengths. Five are piecewise-linear infrastructure the source treats as routine: closure of $\mathrm{PLF}(\mathbb{R})$ under composition and under inverse, the same two for slope $1$ at each end, and finiteness of the number of components of a support. Five more are steps the source asserts without proof — that the line carries no non-fixed periodic points, that a map fixing a set's complement preserves its components, that the iterated images of a pushed-forward interval are pairwise disjoint, that the closure of a commutator's moved set stays inside the union of the two supports (p. 495), and that the derived subgroup of a free group of rank two is non-abelian (p. 494). The last is not from the source at all — that an abelian subgroup of a free group is cyclic, which is what lets the goal finish through Nielsen–Schreier.

Significance

The theorem closes the standard route to proving a group non-amenable. To show a group amenable the classical routes are elementary amenability and subexponential growth, and $F$ is neither elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) nor of subexponential growth, having exponential growth (their Corollary 4.7). To show a group non-amenable the standard route is to exhibit a free subgroup of rank $2$ — the route this theorem closes. $F$ sits in the gap, which is why its status has survived sustained attention.

The result reaches past $F$. Monod's groups of piecewise projective homeomorphisms are counterexamples to von Neumann's conjecture, and Monod's theorem that they contain no non-abelian free subgroup is, in Monod's words, "a sequacious generalization of the corresponding theorem of Brin–Squier about piecewise affine transformations"; of its own proof that paper says it will "largely follow [Brin–Squier, § 3]".

What formalizing it adds. Mathlib has no piecewise-linear maps and no amenability predicate for groups. This mission builds the piecewise-linear layer: a workable $\mathrm{PLF}(\mathbb{R})$, its closure properties, and the structure of supports.

Difficulty

The obstruction is bookkeeping across two finiteness facts of different kinds. Finiteness of the breakpoint set is what gives an element slopes at $\pm\infty$ at all, and what makes two elements affine on each side of a common fixed point. Compactness is the other — throughout, $[f,g] = fgf^{-1}g^{-1}$ — and it splits: that the closure of $\operatorname{supp}[f,g]$ is compact needs only slope $1$ at each end, with no piecewise linearity at all, which is why (2.14b) is formalized under a weaker hypothesis than the source's; that the closure stays inside $\operatorname{supp} f \cup \operatorname{supp} g$ is what reaches back to finiteness. Keeping straight which fact does which job is most of the work.

The first idea a newcomer has about (3.2) is the wrong one. Its proof produces a family of commuting elements, and it is not disjointness of supports that makes them commute: only their intersections with one chosen component are disjoint, and commutation is deduced instead from a minimality argument. A proof routed through disjoint supports will not close.

Formalization scope

What the Lean fixes. Elements are order isomorphisms of $\mathbb{R}$ — strictly increasing bijections, automatically homeomorphisms — rather than a homeomorphism type. Composition follows Mathlib's convention $(f\cdot g)(x) = f(g(x))$, the opposite of the source's right action, so the conjugation identity reads $\operatorname{supp}(fgf^{-1}) = f(\operatorname{supp} g)$ here; getting this backwards states a different theorem that still compiles. A support is the bare moved set, with no closure taken. Piecewise linearity is a finite breakpoint set together with local affineness off it — the set need not be minimal and may be empty. A copy of $\mathbb{Z}^2$ is an injectivity statement about $(m,n)\mapsto u^m v^n$, not a subgroup isomorphism, and the goal is about a single pair $f,g$ rather than a subgroup. The dichotomy hypothesises slope $1$ at both ends directly, not membership in a derived subgroup — that these coincide is the source's result, and both inclusions are formalized here: (2.14a) gives one, and the identification asserted on p. 493 gives the other. Beyond a workable $\mathrm{PLF}(\mathbb{R})$, the development needs Nielsen–Schreier, already in Mathlib as subgroupIsFreeOfIsFree: it is what lets an abelian subgroup of a free group be cyclic, and so lets the goal finish without the source's metabelian ending. That ending is formalized too, as Corollary (3.3) together with the p. 494 remark that the derived subgroup of a free group of rank two is non-abelian; the goal simply does not route through it.

One trivializing reading is ruled out. Slope $1$ at both ends is not a compact-support condition — every translation satisfies it — so (3.2) is not secretly a statement about compactly supported maps.

Nothing is built for $F$ specifically, and amenability is not touched. That is the one piece deliberately omitted, and contributions are welcome on it: modelling $F$ and embedding it in $\mathrm{PLF}(\mathbb{R})$. The piecewise-linear layer is reusable beyond this theorem — Thompson's groups $T$ and $V$, and piecewise-linear topology generally, need exactly it.

Selected references

• M. G. Brin and C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. math. 79 (1985), 485–498, doi:10.1007/BF01388519. Theorem (3.1) is the goal.
• J. W. Cannon, W. J. Floyd and W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Mathématique 42 (1996), 215–256. Theorem 4.10 and Corollary 4.7.
• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013), 4524–4527, arXiv:1209.5229.
• A. Yu. Ol'shanskii and M. V. Sapir, Non-amenable finitely presented torsion-by-cyclic groups, Publ. Math. IHÉS 96 (2002), 43–169, doi:10.1007/s10240-002-0006-7.
• Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016), 177–200, doi:10.4171/ggd/347.
• V. Guba, Amenability problem for Thompson's group $F$: state of the art, J. Groups Complex. Cryptol. 15 (2023), arXiv:2305.07113.