Dynamical Systems

Motivation and historical timeline

In 1915, George D. Birkhoff proved the existence of a retrograde periodic orbit in each bounded component of the planar circular restricted three-body problem and asked whether its double cover bounds a disk-like global surface of section. Such a surface turns a three-dimensional flow into a two-dimensional return map and was intended as a route to a direct periodic orbit (Birkhoff 1915; Liu--Salomão, Section 1.4). McGehee obtained the corresponding section in the small-mass perturbative regime in 1969, while modern contact and symplectic methods recast the question in terms of regularized energy hypersurfaces and Reeb dynamics (Joung--van Koert, Introduction).

In 2012, Hryniewicz established the global-section criterion later quoted by Joung and van Koert: on a dynamically convex star-shaped hypersurface, the proposed binding orbit must be unknotted with self-linking number −1 (Joung--van Koert, Theorem 1.3; Hryniewicz). In 2025, Joung and van Koert combined that criterion with validated orbit and convexity computations for $0\leq\mu\leq 1/2$ and $2.1\leq c\leq 2.1+10^{-6}$ (Theorems 1.2 and 1.5). In May 2026, Liu and Salomão proved the conjecture at every subcritical energy for mass ratios sufficiently close to $1/2$, in fact obtaining rational open books bound by every retrograde orbit in that regime (Theorem 1.16). Their June 2026 Hill result covers every subcritical energy in Hill's lunar problem, which is a limiting model rather than a finite-mass instance of the circular restricted problem (Liu--Salomão 2026). These results leave the universal finite-mass, all-subcritical statement below as the open target.

Setting

Two primaries of masses $1-\mu$ and $\mu$, with $0<\mu<1$, are fixed in rotating coordinates at $(-\mu,0)$ and $(1-\mu,0)$. For a massless particle with phase coordinates $(q_1,q_2,p_1,p_2)$, the Hamiltonian is

$$H_\mu(q,p)=\frac{p_1^2+p_2^2}{2}+q_1p_2-q_2p_1 -\frac{1-\mu}{\sqrt{(q_1+\mu)^2+q_2^2}} -\frac{\mu}{\sqrt{(q_1-1+\mu)^2+q_2^2}}.$$

This is equation (1.1) of Joung--van Koert. Let $h_1(\mu)=H_\mu(L_1)$ be the smallest collision-free critical value, where $L_1$ lies between the primaries. The subcritical range is $H_\mu=-c<h_1(\mu)$; there are then two bounded physical components, one around each primary (Liu--Salomão, Section 4).

The mission labels the primary at $(-\mu,0)$. With complex Levi-Civita variables $z=z_1+iz_2$ and $w=w_1+iw_2$, the inverse position map is $q+\mu=2z^2$, and the regularized Hamiltonian is

$$\begin{aligned} K_{\mu,c}(z,w)={}&\frac{|w|^2}{2}+c|z|^2-\frac{1-\mu}{2} +2|z|^2(z_1w_2-z_2w_1)\\ &-\mu(z_1w_2+z_2w_1) -\frac{\mu|z|^2}{|2z^2-1|}. \end{aligned}$$

On the collision-free domain, $K_{\mu,c}=|z|^2(H_\mu+c)$, and its zero level regularizes collision with the labeled primary (Joung--van Koert, equation (2.2)). The selected component $\Sigma_{\mu,c}$ is anchored at $(z,w)=(0,\sqrt{1-\mu})$. Below $h_1$, it is a star-shaped three-sphere, invariant under the free antipodal deck map $(z,w)\mapsto(-z,-w)$, and it double-covers the corresponding Moser-regularized $\mathbb{R}P^3$ component (Joung--van Koert, Proposition 2.4).

Target

For every $0<\mu<1$, every $-c<h_1(\mu)$, and every complete flow $\varphi$ on $\Sigma_{\mu,c}$ generated by $X_{K_{\mu,c}}$ and commuting with the antipodal map, prove

$$\exists\,\delta\quad \operatorname{GeometricRetrograde}(\delta)\ \land\ \operatorname{RationalGSS}(\operatorname{DoubleLift}(\delta)).$$

Here $\delta$ consists of $x\in\Sigma_{\mu,c}$ and a quotient period $P>0$ with $\varphi_P(x)=-x$, with no earlier positive time reaching either $x$ or $-x$. Its physical projection is required to be a $q_2$-symmetric, simple, collision-free loop of winding $+1$ around the labeled primary. Traversing it twice gives a least-period closed orbit upstairs. This records the geometric retrograde orbit used in the Birkhoff-conjecture formulation; it does not impose the stronger pointwise astronomical monotonicity test distinguished in Joung--van Koert, Definition 2.1, Proposition 2.2, and Remark 2.3.

The rational page is encoded by a smooth immersive disk lift $\widetilde f:D^2\to\Sigma_{\mu,c}$. Its lift is embedded, its interior is transverse to $X_{K_{\mu,c}}$, and its boundary is the closed double lift. After passing to the antipodal quotient, the interior remains embedded and the only nontrivial fibers are antipodal boundary pairs; hence the boundary maps exactly two-to-one onto the prime quotient orbit. Every nonbinding quotient trajectory must meet the page interior at arbitrarily large positive and negative times, matching the recurrence clause in the standard definition of a global surface of section (Hryniewicz, Definition 1.1).

Significance

A global surface of section replaces the continuous three-dimensional regularized flow, away from its binding, by the iterates of a two-dimensional first-return map. Periodic points, invariant sets, and recurrence of that map encode periodic and recurrent trajectories of the original system. This is why Birkhoff connected the conjecture to the existence of a direct orbit, and why later work uses such sections to obtain global dynamical consequences (Birkhoff 1915; Joung--van Koert, Introduction). A proof across all finite mass ratios and all subcritical energies would close the gap between the known perturbative, near-equal-mass, and narrow validated regimes.

Difficulty

Existence of a $q_2$-symmetric geometric retrograde orbit is not the unresolved step: Birkhoff's shooting argument supplies one in each bounded component for every $0<\mu<1$ and every energy below $L_1(\mu)$ (Liu--Salomão, Theorem 5.1). The difficult assertion is global. One must produce a disk with the correct two-fold boundary behavior, prove transversality at every interior point, and prove that every other trajectory returns to it indefinitely in both time directions. Known proofs obtain these conclusions from convexity, dynamical convexity, and pseudo-holomorphic-curve machinery only in restricted parameter ranges (Joung--van Koert, Theorem 1.5; Liu--Salomão, Theorem 1.16).

Formalization scope

The Lean model uses total real-valued extensions of the displayed Hamiltonians, but every physical assertion carries explicit collision-free or denominator guards. The first critical value is initially an infimum; a separate theorem row proves nonemptiness, boundedness below, and attainment at an inner Lagrange point. The energy component is selected by a concrete regularized collision point, the physical mass range is strict, and the headline theorem assumes an actual Flow together with its Hamiltonian-generator and antipodal-equivariance properties. These choices prevent singular derivatives, an unintended component, an empty critical set, or an arbitrary dynamics from satisfying the goal vacuously.

The antipodal quotient in Lean is presently the topological quotient by the explicit deck relation. The formal rational-page predicate is therefore a cover-lift encoding: continuity, the real-action laws, exact quotient fibers, primeness, and global returns are stated downstairs, while smoothness, immersion, and transversality are stated on the Levi-Civita lift. It does not install a smooth atlas or explicit Moser coordinates on the quotient, and it asks for one rational page rather than a full open-book fibration. The theorem concerns one labeled primary; it does not simultaneously assert the analogous result on the other bounded component. The Hill limiting problem and the pointwise astronomical sign condition are not part of the headline conclusion.

All theorem rows are Lean declarations ending in by sorry. Successful elaboration verifies that the statements are syntactically and type-theoretically coherent; it is not evidence that the open theorem has been proved. Supporting rows isolate analytic facts, regularization identities, component geometry, quotient descent, the known retrograde-orbit theorem, and the parameter ranges already covered in the cited literature.

Selected references

• G. D. Birkhoff, The restricted problem of three bodies, Rendiconti del Circolo Matematico di Palermo 39 (1915), 265--334. DOI.
• U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), 1859--1931. arXiv:0812.4076v8.
• C. Joung and O. van Koert, Computational symplectic topology and symmetric orbits in the restricted three-body problem, Nonlinearity 38 (2025), 025015. arXiv:2407.19159v3.
• L. Liu and P. A. S. Salomão, Finite energy foliations and global dynamics in the restricted three-body problem, arXiv:2506.17867v2 (25 May 2026). Preprint.
• L. Liu and P. A. S. Salomão, Birkhoff conjecture and finite energy foliations in Hill's lunar problem, arXiv:2606.12912 (2026). Preprint.

Motivation

The iteration of a rational map $f:\hat{\mathbb C}\to\hat{\mathbb C}$ of the Riemann sphere is the model problem of holomorphic dynamics. The subject was founded by Fatou and Julia around 1918–1920, who split the sphere into a region of stable behaviour and a region of chaotic behaviour, and it was revived in the 1980s by Douady, Hubbard, Sullivan and Thurston. John Milnor's textbook Dynamics in One Complex Variable (3rd ed., Princeton, 2006) is the standard graduate introduction. This mission, the first of a series on the book, formalizes the chain of results that leads from Montel's theorem on normal families to Sullivan's theorem that rational maps have no wandering domains.

Timeline of the results formalized here:

• 1912–1927, Montel. Families of holomorphic maps omitting three values are normal (Milnor, Theorem 3.7).
• 1918–1920, Fatou and Julia. Definition of the Fatou and Julia sets; the Julia set of a map of degree $d\ge2$ is nonempty and equals the closure of the repelling periodic points (Milnor, Lemma 4.8 and Theorem 14.1).
• 1920s–1942. Fatou classified the possible dynamics on an invariant Fatou component; Siegel (1942) showed that Siegel disks exist, and Herman (1979) constructed Herman rings. Together these give the four cases of Milnor's Theorem 16.1.
• 1985, Sullivan. Every Fatou component is eventually periodic (Sullivan, Quasiconformal homeomorphisms and dynamics I, Ann. of Math. 122 (1985); Milnor, Theorem 16.4).

Setting

The Riemann sphere is $\hat{\mathbb C}=\mathbb C\cup\{\infty\}$, the one-point compactification of $\mathbb C$, with the two coordinates $z$ (near finite points) and $1/z$ (near $\infty$). A rational map is $f=p/q$ with $p,q$ coprime complex polynomials, $q\neq0$; it acts on $\hat{\mathbb C}$ in the usual way, and its degree is $d=\max(\deg p,\deg q)$. Write $f^{\circ n}$ for the $n$-th iterate.

A family of maps from an open set to $\hat{\mathbb C}$ is normal if every sequence in it has a subsequence converging locally uniformly in the spherical (chordal) metric. The Fatou set $F(f)$ is the set of points having a neighbourhood on which the iterates $\{f^{\circ n}\}$ form a normal family; the Julia set is its complement $J(f)=\hat{\mathbb C}\setminus F(f)$. A Fatou component is a connected component of $F(f)$. A periodic point $z_0=f^{\circ m}(z_0)$ of minimal period $m$ has multiplier $\lambda=(f^{\circ m})'(z_0)$, computed in a local coordinate; it is repelling if $|\lambda|>1$ and attracting if $|\lambda|<1$.

A Fatou component $U$ with $f(U)=U$ is a Siegel disk (resp. Herman ring) if $f|_U$ is conformally conjugate to an irrational rotation of the unit disk (resp. of a round annulus $\{1<|w|<r\}$).

Formalization targets

Goal: no wandering domains (Theorem 16.4)

For a rational map $f$ of degree $d\ge2$ and every Fatou component $U$ there are $n\ge0$, $p\ge1$ with

$$f^{\circ p}\bigl(f^{\circ n}(U)\bigr)=f^{\circ n}(U).$$

Milestones

1. Lemma 2.5: $\hat{\mathbb C}\setminus\{0,1,\infty\}$ is covered holomorphically by the unit disk.
2. Corollary 3.3 (case $\mathbb D\to\mathbb C\setminus\{0,1\}$): holomorphic maps between hyperbolic surfaces form a normal family.
3. Lemma 3.5 (case $\mathbb C\setminus\{0,1\}\subset\hat{\mathbb C}$).
4. Theorem 3.7 (Montel): holomorphic maps from a domain to $\hat{\mathbb C}$ omitting three values form a normal family.
5. Lemma 4.3: $z\in J(f)\iff f(z)\in J(f)$.
6. Lemma 4.4: $J(f^{\circ k})=J(f)$ for $k>0$.
7. Lemma 4.8: $J(f)\neq\emptyset$ when $d\ge2$.
8. Theorem 14.1: $J(f)=\overline{\{\text{repelling periodic points}\}}$ when $d\ge2$.
9. Theorem 16.1: an invariant Fatou component is an attracting basin, a parabolic basin, a Siegel disk or a Herman ring.

Significance

The results. Montel's theorem is the engine of the Fatou–Julia theory: nonemptiness of $J$, density of iterated preimages and density of repelling cycles all rest on it. Theorem 14.1 identifies the non-normality locus with the closure of the repelling cycles, the form in which the Julia set is usually computed and pictured. Sullivan's theorem, combined with Theorem 16.1, gives a complete qualitative picture of the dynamics on the Fatou set; it is used throughout the later theory, e.g. to show that the Julia set of a postcritically finite map without superattracting cycles is the whole sphere (Milnor, Corollary 16.5).

Formalizing them. All results here are classical theorems with published proofs; none is open. A text search of Mathlib at the platform's pinned revision (0df444a) finds no Montel theorem for families of holomorphic maps, no Fatou or Julia sets and no wandering-domain results; it does contain the Schwarz lemma and the hyperbolic metric on the upper half-plane. The remaining work is to formalize the known proofs.

Difficulty

The early milestones need the uniformization-type input that $\mathbb C\setminus\{0,1\}$ is covered by the disk (via the modular function or an equivalent construction) and Schwarz–Pick-type estimates on hyperbolic surfaces; Mathlib has the Schwarz lemma and the hyperbolic metric of the upper half-plane, but not the Poincaré metric of general hyperbolic domains or covering-space uniformization. Theorem 14.1 requires a quantitative use of Montel's theorem around points of $J$ that are not critical values. Theorem 16.1 needs the Denjoy–Wolff-type classification of self-maps of hyperbolic surfaces and the Snail Lemma for parabolic points. The goal is substantially harder: Sullivan's proof uses the measurable Riemann mapping theorem (Morrey–Ahlfors–Bers) to build an infinite-dimensional family of quasiconformal deformations of $f$, contradicting the finite dimensionality of the space of rational maps of degree $d$. The theory of quasiconformal maps and Beltrami equations is absent from Mathlib, and no elementary argument avoiding it is known.

Formalization scope

All declarations live in the book-wide namespace MilnorDynamics and build on the published definition files MilnorDynamics_NormalFamilies, MilnorDynamics_RationalMaps and MilnorDynamics_PeriodicPoints; one new definition file, MilnorDynamics_FatouComponents, adds Fatou components, immediate basins, Siegel disks and Herman rings.

• $\hat{\mathbb C}$ is OnePoint ℂ; a rational map is a structure of coprime polynomials $p,q$ with $q\ne0$, acting on OnePoint ℂ via RationalMap.toFun; the degree is $\max(\deg p,\deg q)$.
• Holomorphy of a map into $\hat{\mathbb C}$ on an open $U\subseteq\mathbb C$ is continuity plus complex differentiability in the charts $z$ and $1/z$ (IsHolomorphicOn). Normality is locally uniform subconvergence in the chordal metric (IsNormalFamily); the Fatou set is defined through the standard charts of $\hat{\mathbb C}$.
• Multipliers are derivatives of $f^{\circ m}$ in the standard chart at the periodic point, $m$ the minimal period.
• Montel's theorem is stated for a domain $U\subseteq\mathbb C$ rather than an arbitrary Riemann surface (normality is local, Milnor Problem 3-e); Lemma 2.5, Corollary 3.3 and Lemma 3.5 are linked in the special cases used for Montel's theorem.
• The degree hypotheses are Milnor's: $d\ge1$ (nonconstant) in §4 Lemmas 4.3–4.4, $d\ge2$ elsewhere. Without $d\ge2$ several statements are false (e.g. $J(z\mapsto 2z)=\emptyset$), so the hypothesis must not be dropped.

Welcome contributions: the Poincaré metric and Schwarz–Pick on hyperbolic domains, the modular covering of $\mathbb C\setminus\{0,1\}$, the degree theory of rational maps, quasiconformal maps and the measurable Riemann mapping theorem. These are reusable far beyond this mission.

Selected references

• J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. https://doi.org/10.1515/9781400835539
• D. Sullivan, Quasiconformal homeomorphisms and dynamics I. Solution of the Fatou–Julia problem on wandering domains, Ann. of Math. 122 (1985), 401–418. https://doi.org/10.2307/1971308
• L. Carleson and T. W. Gamelin, Complex Dynamics, Universitext, Springer, 1993. https://doi.org/10.1007/978-1-4612-4364-9
• P. Montel, Leçons sur les familles normales de fonctions analytiques et leurs applications, Gauthier-Villars, Paris, 1927.

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

This mission formalizes the question whether the group $\mathrm{IET}$ of interval exchange transformations is amenable, Question 1.6 of Juschenko, Matte Bon, Monod and de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, p. 4 (doi:10.1017/etds.2016.32), together with the landmark results of the literature on the question.

Motivation

An interval exchange transformation cuts the circle $\mathbf R/\mathbf Z$ into finitely many arcs and puts them back in a different order. These maps model the dynamics of polygonal billiards with rational angles, and since Katok–Stepin (1967) and Keane (1975) they have been a central object of ergodic theory. Under composition they form a group, $\mathrm{IET}$. Two questions about this group are open: whether it contains a non-abelian free subgroup (Katok's question), and whether it is amenable, that is, whether it carries a finitely additive, translation-invariant probability measure on all of its subsets. Amenability would answer Katok's question in the negative, since an amenable group has no non-abelian free subgroup.

Timeline.

• 1967: Katok and Stepin first consider exchanges of three or more intervals (JMMS, p. 4).
• 1975: Keane introduces interval exchange transformations systematically and the terminology (doi:10.1007/BF01236981).
• 2009: Novak shows that cyclic subgroups of $\mathrm{IET}$ are undistorted (doi:10.3934/jmd.2009.3.379).
• 2013: Dahmani, Fujiwara and Guirardel show that two generic interval exchange transformations do not generate a free group (doi:10.4171/GGD/209).
• 2013: Juschenko and Monod prove that the topological full group of every minimal Cantor system is amenable, which gives the first finitely generated infinite simple amenable groups (doi:10.4007/annals.2013.178.2.7). The technical core is the case $X = \mathbf Z$ of the lamplighter question for the wobbling group below (Juschenko–de la Salle, p. 2).
• 2013: de Cornulier's Bourbaki exposé records that “La question de la moyennabilité du groupe entier IET est ouverte” (p. 1064-04; published 2014, arXiv:2002.09342).
• 2013: Juschenko, Nekrashevych and de la Salle prove that recurrent actions are extensively amenable (arXiv 2013; published 2016, doi:10.1007/s00222-016-0664-6).
• 2013: Juschenko and de la Salle prove that the lamplighter action of the wobbling group of a recurrent metric space of bounded geometry, for instance $\mathbf Z$ or $\mathbf Z^2$, is amenable, and that it is not when the space contains a Lipschitz injective image of the binary tree; the case $\mathbf Z^d$, $d \ge 3$, is left open (arXiv 2013; published 2015, doi:10.36045/bbms/1432840864).
• 2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, show that a subgroup of $\mathrm{IET}$ is amenable if and only if its action on $\mathbf R/\mathbf Z$ is extensively amenable, prove that every subgroup of rational rank at most $2$ is amenable, and show that finitely supported random walks are Liouville in rank $1$ and are not in rank at least $3$ (arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
• 2017: Dahmani, Fujiwara and Guirardel prove that every finitely generated torsion-free solvable subgroup of $\mathrm{IET}$ is virtually abelian (arXiv 2017; published 2020, doi:10.5802/afst.1641).
• 2018: Garban shows that the action of the wobbling group of a bounded degree graph is diffuse-extensively amenable if and only if the graph is recurrent, and conjectures that $W(\mathbf Z^d) \curvearrowright \mathbf Z^d$ is not extensively amenable for $d \ge 3$ (arXiv 2018; published 2020, doi:10.4171/GGD/567).
• 2026: Guelman and Liousse record (p. 2) that “there is no known example of non amenable or torsion-free non virtually abelian finitely generated iet-group” (arXiv:2601.23054). The question remains open as of 2026.

Setting

Write $\mathbf R/\mathbf Z$ for the circle (UnitAddCircle). A permutation $g$ of $\mathbf R/\mathbf Z$ is an interval exchange transformation (IntervalExchange.IsIntervalExchange g) when it is right-continuous, has finitely many points of discontinuity, and has finitely many angles $g(x) - x$. Equivalently, $g$ cuts the circle into finitely many half-open arcs and translates each of them. The group $\mathrm{IET}$ (IntervalExchange.IET) is the subgroup of permutations of $\mathbf R/\mathbf Z$ that they generate; a milestone states that it consists of the interval exchange transformations themselves. For a subgroup $G \le \mathrm{IET}$, the angle group $\Lambda(G)$ (angleGroup G) is the subgroup of $\mathbf R/\mathbf Z$ generated by all angles of elements of $G$, and the rational rank $\mathrm{rk}_{\mathbf Q}$ (rationalRank) of a subgroup of $\mathbf R/\mathbf Z$ is the supremum of the $d$ such that $\mathbf Z^d$ embeds in it. For a subgroup $\Lambda$ of $\mathbf R/\mathbf Z$, $\mathrm{IET}(\Lambda)$ (IETOf Λ) consists of the elements of $\mathrm{IET}$ all of whose angles lie in $\Lambda$.

A mean on a set $S$ is a function $m$ from the subsets of $S$ to $[0, \infty]$ with $m(\emptyset) = 0$, $m(A \cup B) = m(A) + m(B)$ for disjoint $A, B$, and $m(S) = 1$. A group $G$ is amenable (Garrido.IsAmenable G) when it carries a mean with $m(gA) = m(A)$ for all $g \in G$ and $A \subseteq G$. An action of $G$ on a set $X$ is amenable (IsAmenableAction G X) when $X$ carries a $G$-invariant mean, and extensively amenable (IsExtensivelyAmenable G X) when the finite subsets of $X$ carry a $G$-invariant mean that, for each finite $E_0 \subseteq X$, gives full weight to the finite sets containing $E_0$.

The milestones use further notions, defined precisely in the definitions item and in their own statements:

• A finitely supported probability measure $\mu$ on $G$ drives the left random walk $g_n = h_n \cdots h_1$; the inverted orbit of $x_0 \in X$ is $O_n = \{x_0, g_1^{-1}x_0, \dots, g_n^{-1}x_0\}$. The action is recurrent (IsRecurrentAction) when for every symmetric such $\mu$ and every $x_0$, the induced walk $g_n x_0$ returns to $x_0$ with probability $1$.
• For a functor $F$ from finite sets with injections to amenable groups, $F(X)$ (extend F X) is its extension to an arbitrary set $X$ by direct limits, and an action of $G$ on $X$ gives the semidirect product $F(X) \rtimes G$ (FunctorProduct F G X) acting on $F(X)$. The lamplighter case is $F(X) = (\mathbf Z/2\mathbf Z)^{(X)}$ (Lamplighter G X).
• The wobbling group $W(X)$ (wobbling X) of a metric space $X$ consists of the permutations $g$ of $X$ with $\sup_x d(x, gx) < \infty$.

Formalization targets

Goal

$$\mathrm{IsAmenable}(\mathrm{IET}).$$

The question is open. A proof settles it positively and, through von Neumann's theorem, answers Katok's question in the negative; a disproof shows that $\mathrm{IET}$ is not amenable.

Landmarks

The milestones are results from the literature, stated as their sources state them. From Juschenko–Matte Bon–Monod–de la Salle: $\mathrm{IET}$ is a group (p. 4); Lemmas 2.1 and 2.2 on extensive amenability; Theorem 1.3 and Corollary 1.4, the functorial criterion; Proposition 5.3, that a subgroup of $\mathrm{IET}$ is amenable if and only if its action on $\mathbf R/\mathbf Z$ is extensively amenable; Proposition 4.1 and Lemma 4.3, the inverted-orbit reformulations; Theorem 4.2, recurrence implies extensive amenability; Lemma 5.2 and Theorems 5.1 and 1.9, amenability in rational rank at most $2$; and Theorem 1.10, the Liouville dichotomy, with the steps of its proof: Lemma 5.10, Proposition 5.11 with Lemma 5.13 (realizing $\mathrm{IET}(\Lambda; \Sigma)$ as the topological full group of a minimal subshift of polynomial complexity), and Matte Bon's theorem for virtually cyclic groups. The external results these proofs cite are milestones too: Kesten's criterion for a graph (Woess, Theorem 10.6), Lyons–Peres Theorem 2.17 on rough embeddings, Pólya's theorem (already proved on the platform as MarkovMixing.polya_recurrence), the Baldi–Lohoué–Peyrière comparison lemma, and Matte Bon's Theorem 1.2 on topological full groups of subshifts of slow complexity. From Juschenko–de la Salle: Theorem 1.4 on the wobbling group, with coarse embeddings defined by non-decreasing control functions.

Two further open statements

Garban's question, whether $W(\mathbf Z^d) \curvearrowright \mathbf Z^d$ is extensively amenable for every $d$, and Question 1.11 of Juschenko–Matte Bon–Monod–de la Salle, whether a polynomially growing Schreier graph forces extensive amenability, are stated as open milestones. Each comes with a milestone stating that a positive answer implies the goal.

Significance

The result. A proof would make $\mathrm{IET}$ a natural amenable group containing, by Juschenko–Monod and Juschenko–Matte Bon–Monod–de la Salle, finitely generated infinite simple amenable groups, and would answer Katok's question. A disproof would give the first non-amenable finitely generated group of interval exchange transformations; by Theorem 1.9 it would have rational rank at least $3$.

Formalizing it. The definitions of extensive amenability, of the functorial semidirect products $F(X) \rtimes G$, of inverted orbits and recurrent actions, and of wobbling groups are reusable beyond this mission, as are the external probabilistic results (Kesten's criterion, rough embeddings and recurrence). Pólya's theorem is already formalized and proved on the platform (MarkovMixing.polya_recurrence). None of the other landmarks is formalized.

Difficulty

Every known amenability proof for subgroups of $\mathrm{IET}$ passes through Proposition 5.3 and then needs extensive amenability of the action on the circle. The available criterion for extensive amenability is recurrence of the Schreier graphs, which embed into lattices $\mathbf Z^d$ with $d$ the rational rank; for $d \ge 3$ these graphs can be transient, so recurrence is unavailable. Garban's theorem shows that the natural strengthening of extensive amenability fails for all transient wobbling actions, and Theorem 1.10 shows that the Liouville route fails in rank at least $3$.

Formalization scope

$\mathbf R/\mathbf Z$ is UnitAddCircle, and permutations act on it by evaluation. $\mathrm{IET}$ is defined as the subgroup generated by the interval exchange transformations, so that its group structure needs no proof inside the definitions; a milestone states that nothing else lies in it. The source's precise definition (“a right-continuous permutation $g$ of $\mathbf R/\mathbf Z$ such that the set $\{gx - x, x \in \mathbf R/\mathbf Z\}$, called the set of angles of $g$, is finite”) is read together with its opening phrase, “cutting this circle into finitely many intervals”, so the definition also requires finitely many points of discontinuity: without that requirement a right-continuous permutation with two angles can have infinitely many discontinuities, and the cocycle of Proposition 5.3 would not be finitely supported. Means take values in $[0, \infty]$ and are normalized to total mass $1$. Random walks have finitely supported step distributions $\mu : G \to_0 \mathbf R$ where the sources say “finitely supported”, and probabilities of events of a walk are finite sums over the step sequences. Recurrence of a Markov chain is return to the starting point with probability $1$, expressed through first-return probabilities. Functors $I \to \mathrm{Amen}$ are Mathlib functors from the wide subcategory of FintypeCat on the injective maps to GrpCat with amenable values, extended to a set $X$ by the filtered colimit over its finite subsets.

The goal admits no trivializing reading: $\mathrm{IET}$ contains the irrational rotations and the non-rotation exchanges, and Garrido.IsAmenable is the standard notion. The external milestones (Kesten, Lyons–Peres, Baldi–Lohoué–Peyrière) are cited results, stated in the form the sources apply; proofs of them are welcome contributions in their own right.

Selected references

• K. Juschenko, N. Matte Bon, N. Monod and M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, doi:10.1017/etds.2016.32, arXiv:1503.04977.
• K. Juschenko and M. de la Salle, Invariant means for the wobbling group, Bull. Belg. Math. Soc. Simon Stevin 22 (2015) 281–290, doi:10.36045/bbms/1432840864.
• K. Juschenko, V. Nekrashevych and M. de la Salle, Extensions of amenable groups by recurrent groupoids, Invent. Math. 206 (2016) 837–867, doi:10.1007/s00222-016-0664-6.
• K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. 178 (2013) 775–787, doi:10.4007/annals.2013.178.2.7.
• C. Garban, Inverted orbits of exclusion processes, diffuse-extensive-amenability, and (non-?)amenability of the interval exchanges, Groups Geom. Dyn. 14 (2020) 871–897, doi:10.4171/GGD/567.
• Y. de Cornulier, Groupes pleins-topologiques [d'après Matui, Juschenko, Monod, ...], Séminaire Bourbaki, exposé 1064, Astérisque 361 (2014) 183–223, arXiv:2002.09342.
• F. Dahmani, K. Fujiwara and V. Guirardel, Free groups of interval exchange transformations are rare, Groups Geom. Dyn. 7 (2013) 883–910, doi:10.4171/GGD/209.
• F. Dahmani, K. Fujiwara and V. Guirardel, Solvable groups of interval exchange transformations, Ann. Fac. Sci. Toulouse Math. 29 (2020) 595–618, doi:10.5802/afst.1641.
• M. Keane, Interval exchange transformations, Math. Z. 141 (1975) 25–31, doi:10.1007/BF01236981.
• C. F. Novak, Discontinuity-growth of interval-exchange maps, J. Mod. Dyn. 3 (2009) 379–405, doi:10.3934/jmd.2009.3.379.
• R. Lyons and Y. Peres, Probability on Trees and Networks, Cambridge University Press, 2016, doi:10.1017/9781316672815.
• W. Woess, Random Walks on Infinite Graphs and Groups, Cambridge University Press, 2000, doi:10.1017/CBO9780511470967.
• N. Matte Bon, Subshifts with slow complexity and simple groups with the Liouville property, Geom. Funct. Anal. 24 (2014) 1637–1659, doi:10.1007/s00039-014-0293-4.
• P. Baldi, N. Lohoué and J. Peyrière, Sur la classification des groupes récurrents, C. R. Acad. Sci. Paris Sér. A–B 285 (1977) A1103–A1104 (no DOI).
• N. Guelman and I. Liousse, Some elementary amenable subgroups of interval exchange transformations, arXiv:2601.23054 (2026).

Motivation

A reentrant line is a queueing network in which every customer follows one fixed route but may return to a station after visiting another one. A manufacturing line can have this pattern when a product revisits the same machine at different processing stages. A station can then have little nominal workload and still face unstable queues under an unfortunate service order. Dai and Weiss studied this gap between nominal capacity and fluid stability for reentrant lines in their 1996 paper. The four-class line associated with Lu and Kumar is their sharp example: its behavior changes at a simple cross-station inequality that is different from either station's ordinary workload constraint.

The paper establishes several positive stability results for other disciplines and networks, then gives an exact boundary for the Lu–Kumar line. Here the exact boundary is the focus. The result concerns fluid models, deterministic large-scale approximations of queue trajectories. It does not assert positive Harris recurrence or transience of the underlying stochastic network in both directions. The paper cites Dai's earlier implication from a stable fluid model to a stable stochastic discipline, but the converse was still open in its concluding discussion (Dai and Weiss 1996, pp. 119 and 133).

Setting

There are four customer classes, encountered in order $1\to2\to3\to4$. Classes $1$ and $4$ use station $1$; classes $2$ and $3$ use station $2$. Each class $k$ has a positive mean service time $m_k$ and service rate $\mu_k=1/m_k$. The external arrival rate is normalized to one. The nominal workloads are $\rho_1=m_1+m_4$ and $\rho_2=m_2+m_3$, both assumed strictly below one. These assumptions say that each station has enough average capacity for its own stages, but they leave the scheduling decision unresolved.

At time $t$, $Q_k(t)\ge0$ is the amount of class-$k$ fluid, and $T_k(t)$ is the cumulative service time devoted to that class. The fluid equations balance the inflow and outflow of each class. Outside fluid enters class $1$ at unit rate; completion of class $k$ feeds class $k+1$ until class $4$ exits. Service times and idle times are nondecreasing, and a station's idle time can increase only when its total queue content is zero. A pair $(Q,T)$ with these properties is a work-conserving fluid solution.

The Lu–Kumar priority discipline gives class $4$ priority over class $1$ at station $1$, and class $2$ priority over class $3$ at station $2$. Its fluid model adds the priority complementarity condition: service capacity available to a priority prefix can be unused only when that prefix has no immediate workload. For either model, fluid stability means that some common time $\delta>0$ empties every admissible solution with $\sum_kQ_k(0)=1$, with all queues remaining zero for $t\ge\delta$. Instability is the negation of this statement; it does not require every solution to diverge.

Formalization targets

Exact threshold

Theorem 5.1 and Remark 1 give two connected classifications, under $m_k>0$, $\rho_1<1$, and $\rho_2<1$:

$$\neg\operatorname{FluidStable}(\text{all work-conserving solutions}) \quad\Longleftrightarrow\quad m_2+m_4\ge1,$$ $$\neg\operatorname{FluidStable}(\text{Lu–Kumar priority solutions}) \quad\Longleftrightarrow\quad m_2+m_4\ge1.$$

The first clause captures the paper's existence of an unstable work-conserving policy: on the unstable side, the named priority discipline supplies one; on the other side, every work-conserving fluid model is stable. The second clause records the particular policy classification stated in Remark 1. Equality belongs to the unstable side: the paper exhibits a periodic nonempty solution there (Dai and Weiss 1996, pp. 125–127).

Supporting targets

The milestones follow the paper's own statements and proof claims. The real-analysis extinction criterion of Lemma 2.2(ii) and the maximum-of-components criterion of Lemma 3.2 provide the stability language. Display (3.2), already available as a proved platform theorem, identifies the derivative of an attained maximum at a regular point. The priority condition (4.4) implies the ordinary work-conserving condition (1.13). The unstable half records one first cycle, one solution with every scaled cycle, and instability of the priority model. The stable half records the authors' explicit parameter choice, the two linear Lyapunov conditions, and stability of every work-conserving fluid solution.

Significance

The threshold says that the two station-load inequalities alone do not characterize stability of all work-conserving service orders. The extra inequality $m_2+m_4<1$ determines when the entire work-conserving fluid class is stable; its failure admits a concrete priority discipline with a nonempty trajectory. At the boundary $m_2+m_4=1$, growth need not be strict: periodic fluid behavior already defeats finite-time stability. The result therefore distinguishes the paper's global stability region from the larger parameter region in which both stations are nominally underloaded (Dai and Weiss 1996, Remark 1, p. 125).

A machine-checked development would give reusable definitions for a four-stage reentrant fluid model, its priority complementarity condition, and the precise unit-initial-state notion of stability. The local Lean statements in this proposal compile, but their proofs remain open. The published maximum-derivative fact is the one already proved platform component used by this mission. The other milestones identify the mathematical work needed to formalize the known 1996 result, rather than presenting the result as a new open conjecture.

Difficulty

The ordinary load test $\rho_i<1$ controls how much service each station needs on average, but it does not control which class receives service when several buffers at a station are nonempty. In the Lu–Kumar priority discipline, serving a high-priority downstream class changes the future arrival pattern seen by the other station. Thus a direct argument from $\rho_1<1$ and $\rho_2<1$ to queue extinction fails. On the stable side, checking a single station's workload is also insufficient: its content may fall while earlier-stage fluid continues to feed it. The paper formulates two linear components and a finite maximum; the challenge is to obtain a uniform negative drift whenever that maximum is positive, including times when one station is empty and the other determines the active component (Dai and Weiss 1996, pp. 126–128).

Formalization scope

Classes and stations are Fin 4 and Fin 2, with zero-based Lean indices: paper class $k$ is Lean index $k-1$. The fixed station map is $(0,1,1,0)$. Service times remain real parameters with explicit positivity hypotheses. Paths are total functions of real time, while equations and conclusions apply only on $t\ge0$. The external arrival rate is one, and initial size is the sum $\sum_kQ_k(0)$, since class contents are nonnegative. The nominal-load assumptions are the two strict inequalities in (5.1). The named priority ranking is a permutation; it encodes only the station-local comparisons that matter.

Conditions (1.13) and (4.4), printed as complementarity or “increases only when empty,” use an equivalent interval-constancy condition in Lean. No extra Lipschitz or continuity assumption is placed on solutions: the fluid equations and monotone capacity constraints are intended to supply that regularity. Derivatives at regular points are represented with HasDerivAt. Lemma 2.2(ii) uses the non-strict bound $\dot g\le-\varepsilon$, the version used by the paper's applications, although its displayed hypothesis prints $\dot g<-\varepsilon$. The p. 127 line involving $G_1$ prints $(1-\theta_2)Q_4$; (5.3) fixes the intended coefficient as $(1-\theta_1)Q_4$.

The goal uses Definition 1.3 exactly: one uniform emptying time for all solutions of unit initial content. An impossible solution predicate, or an instability claim that only asks for a nonzero state at time zero, would not represent the paper's theorem. The mission needs finite-index sum and maximum infrastructure, absolute continuity and almost-everywhere differentiation on nonnegative time, plus elementary algebra of service rates and the cycle scaling. These components can be reused in later fluid-network missions. Contributions that preserve the source's hypotheses and boundary case are welcome.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. DOI: 10.1287/moor.21.1.115.

Motivation

A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.

Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.

Setting

A reentrant line has stations $1,\dots,I$ and classes $1,\dots,K$. Fluid enters class $1$ at rate $1$, moves from class $k$ to class $k+1$ on service, and leaves after class $K$. Class $k$ is served at station $\sigma(k)$ with mean service time $m_k > 0$ and rate $\mu_k = 1/m_k$. The constituency of station $i$ is $C_i = \{k : \sigma(k) = i\}$ and its nominal workload is $\rho_i = \sum_{k\in C_i} m_k$. The traffic condition (1.7) is $\rho_i < 1$ for every $i$.

A fluid model solution is a pair $(Q, T)$: $Q_k(t) \ge 0$ is the fluid in class $k$ at time $t$ and $T_k(t)$ the cumulative service time given to class $k$ by time $t$. They satisfy, for $t \ge 0$,

$$Q_k(t) = Q_k(0) + \mu_{k-1}T_{k-1}(t) - \mu_k T_k(t) \quad (\mu_0 T_0(t) = t),$$

$T_k(0) = 0$ with $T_k$ nondecreasing, and the idle time $U_i(t) = t - B_i(t)$, where $B_i(t) = \sum_{k\in C_i} T_k(t)$, is nondecreasing. The solution is work-conserving if $U_i$ increases only at times when station $i$ holds no fluid. The immediate volume of station $i$ is $W_i(t) = \sum_{k \in C_i} m_k Q_k(t)$.

The line is of Kelly type with station means $\beta_1, \dots, \beta_I$ if $m_k = \beta_{\sigma(k)}$ for every class $k$. Its routing has no immediate feedback if $\sigma(k+1) \ne \sigma(k)$ for every $k < K$. A set of fluid solutions is stable (Definition 1.3) if there is a $\delta > 0$ such that every solution in the set with $|Q(0)| = \sum_k Q_k(0) = 1$ is empty from time $\delta$ on.

Formalization targets

Goal: Theorem 6.1

For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is $\delta > 0$ with

$$\sum_k Q_k(0) = 1 \ \Longrightarrow\ Q_k(t) = 0 \quad \text{for all } t \ge \delta,\ k = 1,\dots,K,$$

for every work-conserving fluid solution $(Q,T)$. The number of classes $K$ is arbitrary, of either parity, and the route may start at either station.

Milestones

The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity $G_i(t) = G_i(0) + |C_i|t - B_i(t)/\beta_i$ for $G_i = \sum_{k\in C_i} Q_k^+$, with $Q_k^+ = \sum_{l\le k} Q_l$; the comparison $W_i(t) = 0 \Rightarrow G_i(t) \le G_j(t)$; and the verification that $G_1, G_2$ meet the hypotheses of Lemma 3.2 with $\varepsilon_i = 1/\beta_i - |C_i|$.

Significance

The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line $1,2,2,2,1,1$ with all means $0.3$), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.

Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.

Difficulty

The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components $G_i = \sum_{k\in C_i}Q_k^+$ each decrease at the constant rate $1/\beta_i - |C_i|$ while station $i$ is busy. When station $i$ is idle, $G_i$ can grow, and the argument then needs the comparison $G_i \le G_j$, which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum $G = \max(G_1, G_2)$ need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd $K$ is not printed ("can be proved similarly"), and the formal goal covers it.

Formalization scope

All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.

• Classes and stations are 0-based (Fin K, Fin I). The paper's class $k$ is Lean k - 1.
• Paths are total functions ℝ → Fin K → ℝ, and every equation is imposed for $t \ge 0$ only. Derivatives are taken at $t > 0$ via HasDerivAt.
• Work conservation (1.13) is stated in interval form: $U_i$ is constant on every interval $[s,t] \subseteq [0,\infty)$ on which station $i$ holds fluid throughout. For the continuous nondecreasing $U_i$ this is equivalent to the paper's Stieltjes condition. Lipschitz continuity of the paths is not assumed, because it follows from the model.
• $m_k > 0$ is an explicit hypothesis. $|Q(0)|$ is $\sum_k Q_k(0)$.
• Stability is Definition 1.3, which constrains only solutions with $|Q(0)| = 1$.
• The paper's Theorem 6.1 says "any work-conserving policy is stable", which is stability of the queueing network (Definition 1.1). Its proof establishes stability of the work-conserving fluid model, and the queueing-level conclusion follows from the cited Theorem 1.1 (Dai 1995). The goal is the fluid statement. Theorem 1.1 and the stochastic model are not formalized.
• Lemma 2.2 (ii) is stated with the hypothesis $\dot g \le -\varepsilon$, where the page prints $<$. This is the form in which every application uses it, and it gives a stronger lemma.
• The drift identity is stated for every Kelly-type line, which implies the printed $K = 2n$ display. The printed "$G_2(t) = G_2(t) + nt - \dots$" is read as $G_2(0) + nt - \dots$.
• Condition (b) and the Lemma 3.2 check are stated for both parities of $K$ and both starting stations. A station with no classes has its $\varepsilon_i$ left free.

The goal must not be trivialized. It quantifies over all work-conserving solutions with $|Q(0)| = 1$, and this set is nonempty: a sorry-free witness with $K = 2$ is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even $K$, or to a route starting at station 1, would weaken it.

Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.

Selected references

• J. G. Dai and G. Weiss, Stability and instability of fluid models for reentrant lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115
• J. G. Dai, On positive Harris recurrence of multiclass queueing networks: a unified approach via fluid limit models, Annals of Applied Probability 5(1), 49–77, 1995. https://doi.org/10.1214/aoap/1177004828
• S. H. Lu and P. R. Kumar, Distributed scheduling based on due dates and buffer priorities, IEEE Transactions on Automatic Control 36(12), 1406–1416, 1991. https://doi.org/10.1109/9.106156
• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, 1979.
• J. G. Dai and J. M. Harrison, Processing Networks: Fluid Models and Stability, Cambridge University Press, 2020. https://doi.org/10.1017/9781108772662

Motivation

Stochastic fictitious play is a basic model of learning in repeated games. Each period every player best responds to the empirical frequencies of the opponents' past play, after the player's payoffs have been hit by a fresh random shock. It was introduced by Fudenberg and Kreps (1993), is a standard object in the theory of learning in games (Fudenberg and Levine, The Theory of Learning in Games, 1998), and underlies the quantal-response and logit-learning models used in experimental economics and multi-agent reinforcement learning. The question is whether the players' beliefs settle down, and on what.

Potential games, in which all players receive the same payoff, cover pure coordination games and, after the usual payoff transformations, congestion games and weighted potential games. For them Hofbauer and Sandholm (Econometrica 70, 2002) proved that stochastic fictitious play converges almost surely, and that under a generic regularity condition the limit is a single linearly stable rest point of the perturbed best response dynamic.

Timeline. Fudenberg and Kreps (1993) and Kaniovski and Young (1995) established convergence in 2×2 games. Benaïm and Hirsch (1999) related the process to its mean ordinary differential equation and proved convergence in some $p$ player, two strategy games. Hofbauer (2000) and Hofbauer and Hopkins (2000) constructed Lyapunov functions for the deterministically perturbed dynamics. Hofbauer and Sandholm (2002) combined these with a representation theorem for random utility models and with Pemantle's (1990) nonconvergence theorem to obtain the result formalized here.

Setting

A $p$ player game has finite strategy sets $S^\alpha = \{0,\dots,n^\alpha-1\}$ and utilities $u^\alpha : S \to \mathbb R$ on pure profiles $S = \prod_\beta S^\beta$. The game is a potential game if $u^\alpha(s) = u^\beta(s)$ for all players and all profiles. Mixed profiles form $\Sigma = \prod_\alpha \Delta S^\alpha$, and player $\alpha$'s payoff vector is $U^\alpha_i(x^{-\alpha}) = \sum_{s:\,s^\alpha=i} u^\alpha(s)\prod_{\beta\ne\alpha}x^\beta_{s^\beta}$.

Player $\alpha$'s payoffs are perturbed by a random vector $\varepsilon^\alpha$ with a strictly positive density $f^\alpha$ on $\mathbb R^{n^\alpha}$. The choice function is $C^\alpha_i(\pi) = P(\arg\max_j \pi_j + \varepsilon^\alpha_j = i)$, assumed continuously differentiable, and the perturbed best response is $\tilde B^\alpha(x^{-\alpha}) = C^\alpha(U^\alpha(x^{-\alpha}))$.

In standard stochastic fictitious play, shocks $\varepsilon^\alpha_t$ are independent over time and across players. From an arbitrary initial pure profile, at time $t+1$ each player plays a maximizer of $U^\alpha_k(Z_t^{-\alpha}) + (\varepsilon^\alpha_t)_k$, where the beliefs are the time averages

$$Z_t = \frac1t\sum_{u=1}^t \zeta_u .$$

The mean dynamic of this process is the perturbed best response dynamic

$$(P)\qquad \dot x^\alpha = \tilde B^\alpha(x^{-\alpha}) - x^\alpha .$$

A rest point $x^*$ of (P) is hyperbolic if every eigenvalue of $DF(x^*)$ restricted to the tangent space $\prod_\alpha \mathbb R^{n^\alpha}_0$ of $\Sigma$ has nonzero real part, and linearly stable if every such eigenvalue has negative real part. $RP(P)$ and $LS(P)$ denote the rest points and the linearly stable rest points.

By Theorem 2.1 of the paper, $C^\alpha(\pi) = \arg\max_{y\in\operatorname{int}\Delta}(y\cdot\pi - V^\alpha(y))$ for an admissible deterministic perturbation $V^\alpha$, so (P) coincides with the deterministically perturbed dynamic (PV), in which the argmax replaces $C^\alpha$.

Formalization targets

Goal: Theorem 6.1(iii)

For every potential game, every family of densities meeting the conditions above, every probability space, independent shock family and initial profile:

1. if the shocks are smooth enough that the $V^\alpha$ are $C^N$, $N = \sum_\alpha(n^\alpha-1)$, then

$$P\big(\omega(Z_t)\text{ is a connected subset of } RP(P)\big) = 1;$$

2. if every rest point of (P) is hyperbolic and the field of (P) is $C^2$, then

$$P\Big(\lim_{t\to\infty} Z_t \text{ exists and lies in } LS(P)\Big) = 1.$$

Milestones

In attack order: Theorem 2.1 (the representation), Proposition 4.1 (the function $\Pi(x) = \sum_s u^1(s)\prod_\alpha x^\alpha_{s^\alpha} - \sum_\alpha V^\alpha(x^\alpha)$ is a strict Lyapunov function for (PV)), the identification of the critical points of $\Pi$ with the rest points of (PV), Proposition 4.2 ($CR(PV) = RP(PV)$ under $C^N$ smoothness), Proposition 4.3 (under hyperbolicity $RP(PV)$ is finite and equals $CR(PV)$), and Lemmas A.5 and A.4 (a uniform nondegeneracy condition for the noise of the process).

Significance

The result. Theorem 6.1(iii) says that decentralised, boundedly rational learning in common-interest games does not cycle or wander: beliefs converge to a rest point of the perturbed dynamic, and generically to one that is linearly stable, hence a local maximizer of the perturbed potential $\Pi$. Rest points approximate Nash equilibria as the noise vanishes (Proposition 3.1 of the paper), so the theorem is a selection result for equilibria reached by learning. It is also a template for the stochastic-approximation analysis of learning algorithms whose mean dynamic has a Lyapunov function.

Formalizing it. The theorem is proved in the paper, but none of its ingredients is machine-checked: the random utility representation, chain recurrence of flows, Lyapunov arguments for (PV), and the stochastic-approximation step (Benaïm–Hirsch, Benaïm, Pemantle) are all absent from Mathlib and from this platform. A complete development produces a reusable stochastic-approximation layer, not only this theorem.

Difficulty

The obvious argument, "(P) has a strict Lyapunov function, so the process converges to its rest points", fails twice. First, a strict Lyapunov function does not by itself make every chain recurrent point a rest point (the paper cites counterexamples of Akin and of Benaïm); the step needs either Sard's theorem for a $C^N$ function or finiteness of the rest points, and the stochastic-approximation theory controls the process only through the chain recurrent set. Second, convergence to linearly stable points requires showing that the process avoids unstable rest points. This rests on Pemantle's theorem, whose nondegeneracy hypothesis must be verified uniformly over states and directions (Lemma A.4). Neither step follows from the ODE alone: the theorem is about the random process $Z_t$.

Formalization scope

Players are Fin p with p ≥ 2, strategies Fin (n α) with n α ≥ 1, and mixed profiles live in the ambient space (α : Fin p) → Fin (n α) → ℝ, on which every vector field is defined. Choice probabilities are probabilities of strict argmax events under volume.withDensity (f α). The process $Z_t$ is defined pathwise from the shocks, ties broken by the smallest index (a null event), and the theorem quantifies over every probability space and every independent shock family with the given laws. Derivatives of $V^\alpha$ are those of $V^\alpha$ composed with the projection onto the plane $\sum_i y_i = 1$. Eigenvalues are the complex roots of the characteristic polynomial of the derivative restricted to the tangent space of $\Sigma$. Solutions of a dynamic are differentiable curves on $[0,\infty)$ that stay in $\Sigma$, and chain recurrence uses $\varepsilon$-chains with times $t_i \ge 1$.

A formalization about the ODE (P) in place of the process $Z_t$, a fixed noise law such as logit, or convergence to $RP(P)$ in place of $LS(P)$ would prove a different and weaker statement. These are excluded.

Needed infrastructure: the random utility representation (mission I of this series), flows and chain recurrence of $C^1$ vector fields on compact sets, Sard's theorem for real-valued $C^N$ functions, and the stochastic-approximation theorems of Benaïm–Hirsch (1999, Thm 3.3), Benaïm (1999, Props. 5.3 and 6.4) and Pemantle (1990, Thm 1). The last three are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376
• M. Benaïm and M. W. Hirsch, Mixed Equilibria and Dynamical Systems Arising from Fictitious Play in Perturbed Games, Games and Economic Behavior 29, 36–72, 1999. https://doi.org/10.1006/game.1999.0717
• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, 1–68, 1999. https://doi.org/10.1007/BFb0096509
• R. Pemantle, Nonconvergence to Unstable Points in Urn Models and Stochastic Approximations, Annals of Probability 18(2), 698–712, 1990. https://doi.org/10.1214/aop/1176990853
• D. Fudenberg and D. M. Kreps, Learning Mixed Equilibria, Games and Economic Behavior 5, 320–367, 1993. https://doi.org/10.1006/game.1993.1021
• J. Hofbauer and E. Hopkins, Learning in Perturbed Asymmetric Games, Games and Economic Behavior 52, 133–152, 2005. https://doi.org/10.1016/j.geb.2004.06.006

Motivation

Minimum hourly earnings rules for ride-hailing drivers are meant to protect income during periods when drivers spend part of their time idle. A platform pays a wage per hour carrying riders, yet drivers care about earnings per hour logged onto the platform. When many drivers enter after a wage increase, utilization can fall and offset the increase. A regulation that uses the preceding period's utilization to set the next wage can therefore create feedback in the marketplace. Asadpour, Lobel, and van Ryzin model this feedback and identify the exact minimum earnings targets compatible with bounded wages and continuing service (Asadpour, Lobel, and van Ryzin, 2022, §§3–4).

The question matters to marketplace design because a target that cannot be sustained within the model cannot be reached through a bounded wage policy, even if the platform changes prices over time. The theorem separates two economic regimes. When labor supply is tight, the decisive number is the price where demand equals supply. When supply is loose, the decisive number is the greatest revenue the platform can obtain from riders, converted into affordable driver earnings. This mission concerns the paper's threshold theorem and the four lemmas that state its main analytic ingredients.

Setting

In each discrete period $t$, a platform chooses a rider price $p_t\ge0$ and a wage per ride hour $w_t\ge0$. At price $p$, riders demand $D(p)$ hours of trips. At expected hourly earnings $z$, drivers supply $S(z)$ hours. The quantity of completed rides and driver utilization are

$$Q(p,z)=\min\{D(p),S(z)\},\qquad u(p,z)=\frac{Q(p,z)}{S(z)}.$$

Drivers earn wages only while carrying riders. Thus an earnings equilibrium is a positive sequence $z_t$ satisfying $z_t=w_tu(p_t,z_t)$ in every period. The platform's period profit is $\pi(p,w,z)=(p-w)Q(p,z)$. A minimum earnings target $M>0$ requires

$$w_{t+1}\ge\frac{M}{u(p_t,z_t)}.$$

The rule uses utilization in one period to set a wage floor in the next. A policy is stable if its prices and wages are feasible, it satisfies equilibrium and the wage rule, wages have a finite upper bound across all periods, and profit is nonnegative in all but finitely many periods. This definition permits a finite transition with losses but excludes a wage sequence that grows without bound (Asadpour, Lobel, and van Ryzin, 2022, p. 8, Definitions 1–2 and (5)).

The revenue function is $R(p)=pD(p)$, and the labor cost function is $C(z)=zS(z)$. Write $H$ for the inverse of $C$ on positive expenditure. The paper assumes that $D$ is positive, continuous, and strictly decreasing; $S$ is strictly increasing, differentiable, and positive except possibly at zero; $R$ has a unique peak at $p^*$; and demand and supply cross at $w^*$, so $D(w^*)=S(w^*)$ (Asadpour, Lobel, and van Ryzin, 2022, p. 8, Regularity assumptions).

Each theorem in this mission retains these standing assumptions, including when a particular result uses only some of them.

Formalization targets

Exact stability threshold

The goal is Theorem 1 of the paper. For every $M>0$, stability is characterized by

$$\operatorname{Stable}(D,S,M)\quad\Longleftrightarrow\quad M\le z^*,\qquad z^*=\begin{cases}w^*,&p^*\le w^*,\\H(R(p^*)),&p^*>w^*.\end{cases}$$

The equality case $p^*=w^*$ belongs to the first branch. The theorem gives an if and only if statement about all feasible sequences of prices and wages, rather than a condition for one chosen stationary policy (Asadpour, Lobel, and van Ryzin, 2022, p. 11, Theorem 1 and (7)).

Supporting results

The milestones reproduce Lemmas 1–4 and two claims in the Online Appendix. Lemma 1 establishes the inverse labor cost's existence, regularity, and monotonicity. Lemma 2 identifies continuous, unique equilibrium earnings for a given price and positive wage. Lemma 3 states that stability admits a policy with price equal to wage. Lemma 4 rewrites the wage rule in that regime. The appendix claims compare the loose-supply threshold with $w^*$ and show that the tight-supply wage-growth factor exceeds one above $w^*$ (Asadpour, Lobel, and van Ryzin, 2022, pp. 9–10 and Online Appendix p. 4).

Significance

The theorem identifies the full stable range of targets in this model. In the tight-supply case, raising the target above the demand–supply crossing cannot be stabilized by choosing a different sequence of prices. In the loose-supply case, the highest stable target is tied to the cost of supplying drivers at the platform's peak potential revenue. The distinction explains why the same regulation can have different limits across markets with different demand and supply curves (Asadpour, Lobel, and van Ryzin, 2022, p. 11 and Figure 2).

The paper proves this result mathematically. The remaining formalization task is to represent its sequence model and analytic assumptions in Lean and prove the threshold statement and its supporting lemmas there. Its inverse-cost, equilibrium, and policy-stability interfaces can also be reused for the companion results on utilization shocks and static stability in the same paper. Those companion theorems are separate missions in this series.

Difficulty

The short threshold formula hides two distinct obligations: a policy must satisfy the earnings equilibrium and lagged wage rule at every period, while the impossibility direction must exclude every stable feasible policy, including policies that vary prices over time. The equilibrium earnings formula changes regime when supply at the posted wage crosses demand. At the boundary the two formulas must agree, and the argument must still handle wages that approach or cross the demand–supply point. Boundedness and profit conditions also interact with a finite initial period in which profit may be negative.

The paper's printed explanation for one strict inequality in the tight-supply converse is insufficient: two decreasing factors do not determine the direction of their product. The formal target keeps the inequality the paper uses, while the appendix quotation remains as printed (Asadpour, Lobel, and van Ryzin, 2022, Online Appendix p. 4).

Formalization scope

Prices, wages, earnings, demand, supply, cost, and revenue are real valued. The curves' regularity is imposed on $[0,\infty)$; differentiability of supply is imposed on $(0,\infty)$ together with continuity at zero. Revenue is strictly increasing up to $p^*$ and strictly decreasing afterward, encoding the unique peak. The crossing $w^*$ and inverse $H$ are parameters with their characterizing properties, so the statements hold for their uniquely determined values. The inverse is only used at positive costs.

Lean indexes the first period by $0$, so its rule applies to $w_{t+1}$ for every $t\ge0$ and places no floor on $w_0$. The paper starts at period $1$ and likewise leaves the first wage free. “Bounded wages” means a single real upper bound for every period; “all but finitely many periods” is represented by an eventually true condition on $\mathbb N$.

An equilibrium requires $z_t>0$. This explicit domain condition prevents a zero-supply input from making $u=0/0$ and then $M/u=0$ under Lean's total real division, which would make the regulation vacuous. Lemma 2 correspondingly uses $w>0$. Its branch condition $S(w)<D(p)$ agrees with the paper's $w<S^{-1}(D(p))$ wherever that inverse exists and remains meaningful when demand is outside the range of supply. These domain choices are stated with the items they affect. A complete development needs real-analysis facts about continuous strictly monotone functions and inverses, eventual properties of sequences, and elementary bounds on the utilization ratio. Contributions establishing these interfaces or the stated milestones are within scope.

Selected references

• Arash Asadpour, Ilan Lobel, and Garrett van Ryzin, Minimum Earnings Regulation and the Stability of Marketplaces, SSRN preprint 3502607, version of August 24, 2022; published in Manufacturing & Service Operations Management, 2022. SSRN preprint. The local formalization uses the dated preprint's page and theorem numbering.

Motivation

The Friedmann spacetimes (FLRW spacetimes) are the explicit, spatially homogeneous and isotropic solutions of Einstein's field equations on which standard Big Bang cosmology is built. Under a pressureless (dust, $p=0$) equation of state they form a family indexed by a curvature parameter $k$: the critical spacetime $k=0$, the underdense spacetimes $k<0$ and the overdense spacetimes $k>0$. The current $\Lambda$CDM model fits supernova data with the critical Friedmann spacetime plus a cosmological constant (dark energy).

Alexander, Temple and Vogler (arXiv:2510.14228) study how stable the pressureless Friedmann spacetimes are under smooth, spherically symmetric (radial) perturbations near the Big Bang. They write the Einstein–Euler equations in self-similar variables $(\bar t,\xi)$, $\xi=\bar r/\bar t$, a formulation introduced by Smoller, Temple and Vogler (Proc. R. Soc. A, 2017). In these variables the critical Friedmann spacetime is a time-independent solution. They argue that the instability of this rest point causes underdense perturbations to accelerate away from $k<0$ Friedmann spacetimes at intermediate times, and they propose this as a mechanism for the observed acceleration that needs no cosmological constant.

This mission formalizes the dynamical-systems core of that paper: the STV ODE of orders $n=1$ and $n=2$, its rest points and eigenvalues, the exact $k<0$ Friedmann trajectory, and the order-2 instability theorem.

Setting

Expand a solution that is smooth at the centre of symmetry in even powers of $\xi$: $z=\kappa\rho\bar r^2=z_2(\bar t)\xi^2+z_4(\bar t)\xi^4+\dots$ (density) and $w=v/\xi=w_0(\bar t)+w_2(\bar t)\xi^2+\dots$ (velocity). Collecting like powers of $\xi$ gives, at each order $n$, a closed $2n\times 2n$ system $\bar t\,\dot U=F_n(U)$, the STV ODE of order $n$. At order $1$, in the unknowns $(z_2,w_0)$:

$$\bar t\dot z_2=2z_2-3z_2w_0,\qquad \bar t\dot w_0=-\tfrac16z_2+w_0-w_0^2 .$$

At order $2$, in $(z_2,w_0,z_4,w_2)$, the system adds

$$\bar t\dot z_4=\tfrac5{12}z_2^2w_0+4z_4-5w_0z_4-5z_2w_2,\qquad \bar t\dot w_2=-\tfrac1{24}z_2^2+\tfrac14z_2w_0^2-\tfrac1{10}z_4+3w_2-4w_0w_2 .$$

The system is autonomous in log-time $\tau=\ln\bar t$. Its rest points include the Minkowski point $M=(0,1)$, resp. $(0,1,0,0)$, and the critical Friedmann point $SM=(\tfrac43,\tfrac23)$, resp. $(\tfrac43,\tfrac23,\tfrac{40}{27},\tfrac29)$. The $p=0$, $k=-1$ Friedmann spacetime with parameter $\Delta_0>0$ is given in parametric form by $\bar t=\tfrac{\Delta_0}{2}(\sinh2\theta-2\theta)$ and explicit functions $\tilde z_2,\tilde w_0,\tilde z_4,\tilde w_2$ of $\theta>0$ (equations (2.41), (2.43)).

Formalization targets

Goal: Theorem 8 at order $n=2$

Fix $\Delta_0>0$. Let $\mathcal S$ be the set of solutions of the order-2 STV ODE on $\bar t\in(0,\infty)$ that tend to $SM$ as $\bar t\to0^+$, tend to $M$ as $\bar t\to\infty$, and agree exactly with the $k=-1$ Friedmann spacetime at leading order, i.e. $(z_2,w_0)(\bar t)=(\tilde z_2,\tilde w_0)(\theta)$. Then

$$\mathcal S=\{U_b : b\in\mathbb R\},\qquad b\mapsto U_b \text{ injective},\qquad U_0=(\tilde z_2,\tilde w_0,\tilde z_4,\tilde w_2).$$

So the $k<0$ Friedmann spacetime is one member of a one-parameter family of trajectories from $SM$ to $M$. All members agree with it at leading order, and the others differ from it at order 2.

Milestones

1. Corollary 1 at $n=1$: the rest points $U,M,SM$; the eigenpairs $(\tfrac23,(-9,\tfrac32))$ and $(-1,(4,1))$ at $SM$; $M$ is degenerate stable.
2. Corollary 1 at $n=2$: the rest points; the four eigenpairs (2.30)–(2.33) at $SM$; $-1$ is the only eigenvalue at $M$.
3. Equation (2.29): for every $k\ge1$ the block $P_k$ of (2.26) at $SM$ has eigenvalues $\tfrac{2k}3$ and $\tfrac{2k-5}3$.
4. Theorem 5 at $n=1$ and $n=2$: the explicit $k=-1$ Friedmann curve solves the STV ODE and runs from $SM$ to $M$.
5. Theorem 7: solutions tending to $M$ satisfy $z_2,z_4=O(\bar t^{-1})$ and $w_0-1,w_2=O(\bar t^{-1}\ln\bar t)$.
6. Theorem 9 at $n=2$: some solutions that agree with Friedmann at leading order and decay to $M$ blow up as $\bar t\to0^+$ instead of tending to $SM$.

Significance

The result. At order $1$ every relevant trajectory is a Friedmann spacetime. Order $2$ is the first order where the instability of $SM$ (the second positive eigenvalue $\tfrac43$) produces trajectories that agree with a $k<0$ Friedmann spacetime as $\bar t\to0$ and as $\bar t\to\infty$ but differ from it in between. The paper reads this as an acceleration away from Friedmann spacetimes without dark energy. The extra eigenvalue $-\tfrac13$ is why some perturbations do not have a self-similar Big Bang.

Formalizing it. The paper is an announcement: most claims are justified by eigenvalue computations and appeals to standard ODE theory (Hartman–Grobman, decay at degenerate nodes). A machine-checked proof of the order-2 statements would turn these appeals into explicit arguments for a concrete polynomial system. None of these results is known to have been formalized.

Difficulty

The eigenvalue milestones are finite computations. The trajectory milestones (Theorem 5) need hyperbolic-function identities and limits at $\theta\to0^+$, where numerators and denominators both vanish to high order. The goal is harder because it is global. Linearizing at $SM$ only describes trajectories near $SM$. One must also show that every member of the family exists for all time and reaches $M$, and that nothing outside the family belongs to $\mathcal S$. Theorem 7 needs sharp decay rates at a rest point whose Jacobian is not diagonalizable, which is where the logarithm comes from.

Formalization scope

• Phase-space points are vectors Fin 2 → ℝ or Fin 4 → ℝ, with coordinates ordered $(z_2,w_0)$ and $(z_2,w_0,z_4,w_2)$.
• A solution is a map $U:\mathbb R\to\mathbb R^{2n}$ of log-time $\tau=\ln\bar t$ with $U'(\tau)=F_n(U(\tau))$ for every $\tau$. Hence $\bar t\to0^+$ is $\tau\to-\infty$, $\bar t\to\infty$ is $\tau\to+\infty$, and $\bar t=\tfrac{\Delta_0}{2}(\sinh2\theta-2\theta)$ becomes $\tau=\log(\Delta_0\cdot\mathrm{bigBangTime}(\theta))$.
• Jacobians are Fréchet derivatives (fderiv). Norms on $\mathbb R^{4}$ are sup norms.
• The goal requires a family parametrized by $\mathbb R$ that is injective, has range exactly $\mathcal S$, and has $U_0$ equal to the Friedmann curve. Exhibiting a single solution does not prove it.
• Out of scope: the derivation of the STV PDE and STV ODE from the Einstein–Euler equations (Theorems 1–3), the coordinate transformations (Theorems 4 and 6), and the general-order statements of Theorems 8–9. The paper does not write out the order-$n$ system for general $n$, so these cannot be stated without first formalizing that derivation. Contributions in that direction are welcome.
• Discrepancy with the source: Corollary 1 says $\boldsymbol R_M$ is the only eigenvector at $M$. For the explicit order-2 system (2.48)–(2.51) the $-1$ eigenspace at $M$ is two-dimensional, so the order-2 milestone does not include that uniqueness claim.

Selected references

• C. Alexander, B. Temple, Z. Vogler, The Instability of the Critical Friedmann Spacetime at the Big Bang as an Alternative to Dark Energy, arXiv preprint, 2025. https://arxiv.org/abs/2510.14228
• J. Smoller, B. Temple, Z. Vogler, An instability of the standard model of cosmology creates the anomalous acceleration without dark energy, Proc. R. Soc. A 473 (2017). https://doi.org/10.1098/rspa.2016.0887