Motivation

A uniform spanning tree of a finite connected graph is a spanning tree chosen uniformly at random. On an infinite graph one takes limits along finite pieces: the free uniform spanning forest (FUSF) is the weak limit of uniform spanning trees of an increasing sequence of finite connected subgraphs, with no boundary identification. Uniform spanning forests connect random walks, electrical networks, determinantal processes and $\ell^2$-Betti numbers of groups.

A random object on a graph is a factor of IID if it can be produced by one measurable rule from independent uniform labels on the vertices, in a way that commutes with all graph symmetries. Such representations are the measure-theoretic analogue of local algorithms, and they are central in ergodic theory of group actions. Whether the FUSF is a factor of IID was raised by Lyons at Oberwolfach in 2013, and Timár's 2025 paper describes the unrestricted question as open.

Timeline

• 1991. Pemantle constructs infinite-volume uniform spanning trees on $\mathbb Z^d$ (Ann. Probab., 1991; arXiv:math/0404043).
• 2001. Benjamini, Lyons, Peres and Schramm develop the general theory of free and wired uniform spanning forests; on transient graphs the wired forest is a factor of IID via Wilson's algorithm rooted at infinity (doi:10.1214/aop/1008956321).
• 2003. Lyons develops determinantal probability measures on countable sets (doi:10.1007/s10240-003-0016-0).
• 2009. Borcea, Brändén and Liggett introduce strongly Rayleigh measures and their negative-dependence theory (doi:10.1090/S0894-0347-08-00618-8).
• 2013. Lyons discusses the FUSF factor question for Cayley graphs (doi:10.4171/OWR/2013/42).
• 2016. Lyons and Thom prove Bernoulli isomorphism for equivariant determinantal measures on amenable Cayley graphs and ask a broader determinantal factor question (doi:10.1017/etds.2014.70).
• 2022. Nam, Sly and Zhang give FIID codings of free Ising measures on regular trees through Brownian-driven systems (doi:10.1007/s00220-021-04260-2).
• 2025. Timár proves FIID representability of the free forest on recurrent and invariantly amenable unimodular random graphs (doi:10.1007/s11856-025-2884-1).

The source of this mission, an OpenAI preprint dated September 25, 2026, proves the unrestricted statement with one rule for all graphs.

Setting

Let $G$ be an infinite, connected, locally finite, simple, undirected graph. For a finite connected subgraph $H$, let $\mathrm{UST}_H$ be the uniform law on spanning trees of $H$. For finite connected subgraphs $H_1\subseteq H_2\subseteq\cdots$ whose edges exhaust $E(G)$, the laws $\mathrm{UST}_{H_n}$ (edges outside $H_n$ absent) converge weakly; the limit $\mathrm{FUSF}_G$ on $\{0,1\}^{E(G)}$ does not depend on the exhaustion (Proposition 2.2).

A rule $\Phi(G,U,e)\in\{0,1\}$ takes a graph, real vertex labels $U=(U_v)$ and an edge. It is equivariant if $\Phi(\sigma G,\sigma U,\sigma e)=\Phi(G,U,e)$ for every isomorphism $\sigma$, and root independent if it uses no distinguished vertex.

A law $\mu$ on $\{0,1\}^F$, $F$ finite, is strongly Rayleigh if $\sum_x\mu(x)\prod_iz_i^{x_i}\ne0$ whenever all $\operatorname{Im}z_i>0$; on a countable set, every finite marginal must be strongly Rayleigh.

Formalization targets

Milestones (strongly Rayleigh processes, Section 6)

• Lemma 6.1: for strongly Rayleigh $\mu$ and tilts $\mu_h$, $\partial p_i/\partial h_j=\operatorname{Cov}_{\mu_h}(X_i,X_j)$ and $\sum_j|\partial p_i/\partial h_j|\le2p_i(1-p_i)\le\tfrac12$.
• Theorem 1.3: an invariant strongly Rayleigh law on $\{0,1\}^\Gamma$, $\Gamma$ a countable group, is an equivariant factor of IID.
• Inputs to Corollary 1.4: finite determinantal laws with $0\le K\le I$ exist and are strongly Rayleigh; on a countable set the determinantal law of a positive contraction exists and is unique.
• Corollary 1.4: invariant determinantal laws on countable groups are factors of IID, in particular when $K_{gh,gk}=K_{h,k}$.

Goal: Theorem 1.1

$$\exists\ \Phi\ \text{Borel, equivariant, root independent}:\quad \forall G,\quad \{e:\Phi(G,U,e)=1\}\sim\mathrm{FUSF}_G\quad\text{for IID Uniform}[0,1]\ U.$$

The Lean statement OAI.Problem336.fusf_is_factor_iid is open on the platform.

Significance

Theorem 1.1 answers the FUSF factor question without amenability, transience, unimodularity, degree bounds or moment assumptions, and with a single rule for all graphs; Corollary 1.2 gives the factor statement under every unimodular random graph law. Theorem 1.3 and Corollary 1.4 extend the method to all invariant strongly Rayleigh and determinantal processes on countable groups, addressing the regular-action case of the Lyons–Thom question. The paper asserts an ordinary Borel factor, not a finitary one.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. Formalization would also provide uniform spanning trees, the free forest limit, strongly Rayleigh measures and determinantal laws as reusable Lean objects.

Difficulty

Previous constructions use structure that is absent in general: Wilson's algorithm works for the wired forest on transient graphs, and Timár's construction needs monotone limits along a hyperfinite exhaustion. A factor must produce one exact sample of the infinite-volume law while controlling all edges jointly, and equivariance forbids any choice of root or ordering. The paper's route observes the forest through independent Brownian noises and must show that the posterior drift has a uniformly Lipschitz response to the observations even when the fields are unbounded over the graph.

Formalization scope

• Graphs are coded on vertex set $\mathbb N$ by symmetric irreflexive ℕ → ℕ → Bool; edges are pairs $u<v$; a connected graph on $\mathbb N$ is automatically infinite. Equivariance is invariance under every permutation of $\mathbb N$ applied to graph, labels and edge.
• RuleBorel is joint measurability of $\Phi$ in the product σ-algebras.
• IsVertexIID requires the label coordinates to have independent Uniform$[0,1]$ finite-dimensional laws (with $s=\varnothing$ this forces a probability measure).
• HasFUSFLaw asks that every cylinder probability (edges in $A$ present, edges in $B$ absent) be the limit of the corresponding uniform-spanning-tree ratio along every exhaustion by finite connected subgraphs covering all edges.
• The strongly Rayleigh and determinantal milestones use ProbabilityMeasure (Γ → Bool), left translation $(\tau_ga)_h=a_{g^{-1}h}$, i.i.d. labels in Set.Icc 0 1 via Measure.infinitePi, and Hermitian kernels with $0\le\langle c,Kc\rangle\le\|c\|^2$ on finitely supported vectors.

A complete development needs the matrix-tree theorem and Kirchhoff formulas, weak limits on $\{0,1\}^{E}$, Brownian motion and a Borel Picard iteration for the decoder, and the Borcea–Brändén–Liggett theory. Contributions formalizing Proposition 2.2 (free exhaustion limit), Lemma 2.3 (finite-field forest response) and Proposition 4.2 (sampling from independent Brownian paths) are welcome.

Selected references

• OpenAI, The free uniform spanning forest is a factor of IID, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026.pdf
• I. Benjamini, R. Lyons, Y. Peres, O. Schramm, Uniform spanning forests, Ann. Probab., 2001. https://doi.org/10.1214/aop/1008956321
• R. Lyons, ℓ²-Betti numbers, cost, and the free uniform spanning forest, Oberwolfach Reports, 2013. https://doi.org/10.4171/OWR/2013/42
• Á. Timár, Factor of iid's through stochastic domination, Israel J. Math., 2025. https://doi.org/10.1007/s11856-025-2884-1
• R. Lyons, A. Thom, Invariant coupling of determinantal measures on sofic groups, Ergodic Theory Dynam. Systems, 2016. https://doi.org/10.1017/etds.2014.70
• R. Lyons, Determinantal probability measures, Publ. Math. IHÉS, 2003. https://doi.org/10.1007/s10240-003-0016-0
• J. Borcea, P. Brändén, T. M. Liggett, Negative dependence and the geometry of polynomials, J. Amer. Math. Soc., 2009. https://doi.org/10.1090/S0894-0347-08-00618-8
• D. Nam, A. Sly, L. Zhang, Ising model on trees and factors of IID, Comm. Math. Phys., 2022. https://doi.org/10.1007/s00220-021-04260-2
• R. Pemantle, Choosing a spanning tree for the integer lattice uniformly, Ann. Probab., 1991. https://arxiv.org/abs/math/0404043

Motivation

Mixing is the basic notion of asymptotic independence in ergodic theory: a measure-preserving transformation $T$ is mixing if the event $A$ at time $0$ and the event $B$ at time $n$ become independent as $n\to\infty$. Mixing of order $k$ asks the same for $k$ events at times whose gaps all tend to infinity. In 1949 Rokhlin introduced higher-order mixing and asked whether mixing (order $2$) already implies mixing of order $3$, and hence of all orders. The question has been one of the oldest in ergodic theory. It matters because higher-order mixing is the property used to prove multiple recurrence and independence statements, and because for actions of $\mathbb Z^2$ the analogous implication is false.

Timeline

• 1949. Rokhlin introduces higher-order mixing, proves it for ergodic endomorphisms of compact abelian groups, and raises the question for general transformations (mathnet).
• 1967. Furstenberg introduces joinings and disjointness, the language in which failure of higher-order mixing appears as a non-product pairwise-independent joining (doi:10.1007/BF01692494).
• 1978. Ledrappier gives a mixing $\mathbb Z^2$-action that is not mixing of order $3$ (Un champ markovien peut être d'entropie nulle et mélangeant, C. R. Acad. Sci. Paris).
• 1984. Kalikow proves that twofold mixing implies threefold mixing for rank-one transformations (doi:10.1017/S014338570000242X).
• 1991. Host proves mixing of all orders for mixing systems with singular spectrum (doi:10.1007/BF02773866).
• 1993. Ryzhikov proves mixing of all orders for mixing finite-rank actions (doi:10.1007/BF01085983).
• 2006. de la Rue explains why Ledrappier-type "three-dot" counterexamples cannot exist in one dimension (doi:10.1007/s00574-006-0024-z).
• 2008. Janvresse and de la Rue show that certain pairwise-independent joinings force positive entropy (doi:10.1017/S0143385707000958).
• 2024. Bergelson and Zelada show that strongly mixing systems are mixing of all orders along a large set of layouts (doi:10.1017/etds.2023.63); Kanigowski and Ravotti prove multiple mixing for shearing flows (arXiv:2410.13686); Ryzhikov surveys 75 years of the problem (arXiv:2411.07234).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims an affirmative answer for a single invertible transformation.

Setting

Let $(\Omega,\mathcal F,\mu)$ be a probability space and $T:\Omega\to\Omega$ an invertible measurable map with measurable inverse that preserves $\mu$. $T$ is mixing if for all $A,B\in\mathcal F$

$$\mu(A\cap T^{-n}B)\longrightarrow\mu(A)\,\mu(B)\qquad(|n|\to\infty,\ n\in\mathbb Z).$$

For $k\ge2$, $T$ is mixing of order $k$ if for all $A_1,\dots,A_k\in\mathcal F$

$$\mu\Bigl(\bigcap_{i=1}^{k}T^{-t_i}A_i\Bigr)\longrightarrow\prod_{i=1}^{k}\mu(A_i)$$

whenever $t_1<\dots<t_k$ and $\min_i(t_{i+1}-t_i)\to\infty$; by invariance one may take $t_1=0$. The order counts the number of sets (so order $k$ is "multiplicity $k-1$" in Rokhlin's and Ryzhikov's convention).

Formalization targets

Goal: Theorem 1.1

If $T$ is an invertible mixing probability-preserving transformation, then for every $k\ge3$ and all measurable $A_1,\dots,A_k$,

$$\mu\bigl(A_1\cap T^{-n_1}A_2\cap\cdots\cap T^{-(n_1+\cdots+n_{k-1})}A_k\bigr)\longrightarrow\prod_{i=1}^{k}\mu(A_i)\quad\text{as}\ \min(n_1,\dots,n_{k-1})\to\infty,$$

the $n_i$ ranging over positive integers. No standardness or countable-generation assumption is made on $(\Omega,\mathcal F,\mu)$. The Lean statement OAI.Rokhlin.mixing_all_finite_orders is open on the platform.

Significance

The theorem resolves Rokhlin's multiple-mixing problem for one transformation: mixing implies mixing of all orders, with no structural hypothesis (rank, spectrum, algebraic form). It explains the difference between $\mathbb Z$ and $\mathbb Z^2$: Ledrappier's example shows the implication fails for several commuting generators. The paper also derives the conclusion for mixing endomorphisms and for mixing flows with strongly continuous Koopman operators (Corollary 8.1).

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. Given the age and prominence of the problem, an independent formal verification would be valuable.

Difficulty

A failure of threefold mixing produces, in the limit, a joining of three copies of the system that is pairwise independent but not the product. Pairwise independence alone does not force a joining to be a product, so soft joining arguments do not suffice; earlier positive results used rank, spectral or algebraic structure to exclude such joinings. A reduction to zero entropy is available (positive-entropy parts are handled separately), but in zero entropy the non-product joining must be ruled out with no structural information about $T$. In addition, the general (non-standard) probability space prevents direct use of disintegration and Rokhlin–Halmos-type tools without first reducing to a separable factor.

Formalization scope

• $\Omega$ carries an arbitrary MeasurableSpace; $\mu$ has IsProbabilityMeasure; $T$ is a MeasurableEquiv with MeasurePreserving T μ μ.
• timeMap T n is the $n$-th power of $T$ as a permutation, $n\in\mathbb Z$; IsMixing μ T uses the filter comap Int.natAbs atTop on $\mathbb Z$.
• MixingOfOrder μ T k: for every family of measurable sets indexed by Fin k, the measure of $\bigcap_i T^{-\mathrm{layoutTime}(i)}A_i$ tends to $\prod_i\mu(A_i)$ along atTop on Fin (k-1) → ℕ+, where layoutTime gives the partial sums of the gaps.
• The theorem is stated for every $k\ge3$; the case $k=2$ is the hypothesis.

A complete development needs joinings, factor maps and entropy (Pinsker factor), measurable selection or a reduction to standard spaces, and the paper's array and operator machinery. Contributions formalizing the reduction steps (Proposition 2.1, zero-entropy witness) or classical special cases (Kalikow's rank-one theorem) are welcome.

Selected references

• OpenAI, Rokhlin's multiple-mixing problem for one transformation, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Rokhlins-multiple-mixing-problem-for-one-transformation-September-23-2026/paper.pdf
• V. A. Rokhlin, On endomorphisms of compact commutative groups, Izv. Akad. Nauk SSSR Ser. Mat., 1949. https://www.mathnet.ru/eng/im3198
• T. de la Rue, 2-fold and 3-fold mixing: why 3-dot-type counterexamples are impossible in one dimension, Bull. Braz. Math. Soc., 2006. https://doi.org/10.1007/s00574-006-0024-z
• S. A. Kalikow, Twofold mixing implies threefold mixing for rank one transformations, Ergodic Theory Dynam. Systems, 1984. https://doi.org/10.1017/S014338570000242X
• B. Host, Mixing of all orders and pairwise independent joinings of systems with singular spectrum, Israel J. Math., 1991. https://doi.org/10.1007/BF02773866
• V. V. Ryzhikov, Joinings and multiple mixing of finite rank actions, Funct. Anal. Appl., 1993. https://doi.org/10.1007/BF01085983
• V. V. Ryzhikov, Multiple mixing, 75 years of Rokhlin's problem, preprint, 2024. https://arxiv.org/abs/2411.07234
• H. Furstenberg, Disjointness in ergodic theory, minimal sets, and a problem in Diophantine approximation, Math. Systems Theory, 1967. https://doi.org/10.1007/BF01692494

Motivation: Banach's simple Lebesgue-spectrum problem

A measure-preserving transformation $T$ of a probability space acts on square-integrable functions by the Koopman operator $U_Tg=g\circ T$, a unitary operator. Its spectral type (discrete, singular continuous, absolutely continuous) and its multiplicity are basic invariants of ergodic theory. The Lebesgue spectrum is the spectral type of the shift on $\ell^2(\mathbb Z)$, the type of Bernoulli shifts and other strongly chaotic systems, where it occurs with infinite multiplicity. Banach's problem asks whether Lebesgue spectrum can occur with multiplicity one: is there a transformation whose Koopman operator on the orthogonal complement of the constants is unitarily equivalent to multiplication by $w$ on $L^2(S^1)$? Equivalently, is there a single function whose bilateral orbit under $U_T$ is an orthonormal basis of the mean-zero space? The problem combines spectral theory with the construction of explicit dynamics, and a smooth example would show this spectral behavior is compatible with the regularity of differentiable dynamics.

Timeline

• 1949 — Rokhlin asks for ergodic automorphisms with simple, or at least finite-multiplicity, Lebesgue spectrum (Uspekhi Mat. Nauk 1949, §4, no. 7).
• 1960 — Ulam records a real-line form of the question attributed to Banach (A Collection of Mathematical Problems, Interscience, 1960, §6, p. 76).
• 1970 — Anosov and Katok introduce approximation-by-conjugation constructions of smooth ergodic diffeomorphisms (Trudy MMO 1970).
• 1978 — Helson and Parry construct cocycles over aperiodic transformations with associated Lebesgue spectrum (Ark. Mat. 1978).
• 1984 — Mathew and Nadkarni construct a transformation with a Lebesgue component of multiplicity two (Bull. LMS 1984).
• 1999 — Guenais connects Morse cocycles with flat polynomials and constructs a group action with simple spectrum of mixed type (ETDS 1999).
• 2001 — Fayad constructs $C^\infty$ volume-preserving torus diffeomorphisms with simple (not Lebesgue) spectrum (J. LMS 2001).
• 2020–2023 — Prikhod'ko constructs a finite-measure flow with simple Lebesgue spectrum (Sb. Math. 2020); Fayad–Forni–Kanigowski (JAMS 2021) and Abdedou–Fayad–Kessi (DCDS 2023) obtain smooth flows with countable Lebesgue multiplicity; el Abdalaoui presents an infinite-measure conservative example (arXiv:1508.06439). None of these gives a probability-preserving map with simple Lebesgue spectrum on the whole mean-zero space.
• 2026 — The OpenAI preprint A smooth three-torus diffeomorphism with simple Lebesgue spectrum (OpenAI Math Release, September 23, 2026) claims a $C^\infty$ volume-preserving diffeomorphism of $\mathbb T^3$ with this property. It has not been peer reviewed and its theorem is not formally verified.

Setting

Let $\mathbb T=\mathbb R/\mathbb Z$ and let $\mu$ be normalized Lebesgue (Haar) measure on $\mathbb T^3$. A bijection $T:\mathbb T^3\to\mathbb T^3$ is a $C^\infty$ diffeomorphism if $T$ and $T^{-1}$ lift locally to $C^\infty$ maps of $\mathbb R^3$. It is volume preserving if $\mu(T^{-1}A)=\mu(A)$ for every measurable $A$. Let $L^2_0(\mathbb T^3,\mu)$ be the closed subspace of complex square-integrable functions with integral zero, and $U_Tg=g\circ T$. Let $m$ be Haar measure on the circle and $w(z)=e^{2\pi i z}$ the first Fourier character.

In Lean (namespace OAI.ThreeTorus), the torus is Fin 3 → UnitAddCircle with the product Haar measure, smoothness is local smooth lifting on Fin 3 → ℝ, $L^2_0$ is the subspace meanZero of Lp ℂ 2 μ, and MainConclusion packages the theorem below.

Formalization targets

Goal: smooth simple Lebesgue spectrum (Theorem 1.1)

There exist a $C^\infty$ volume-preserving diffeomorphism $T$ of $\mathbb T^3$ and a real-valued $f\in L^2_0(\mathbb T^3,\mu)$ such that

$$\{\,f\circ T^n : n\in\mathbb Z\,\}\ \text{is an orthonormal basis of } L^2_0(\mathbb T^3,\mu);$$

moreover $T$ is ergodic, and there is a unitary $W:L^2_0(\mathbb T^3,\mu)\to L^2(S^1,m)$ with

$$W(g\circ T)=w\cdot W(g)\qquad\text{for all } g\in L^2_0 .$$

The goal is published on the platform with status Open.

Significance

The result itself. The theorem answers the probability-preserving form of Banach's problem, with the strongest kind of example: the invariant measure is the standard smooth volume on a compact manifold, the map is $C^\infty$, and the conclusion covers the whole mean-zero space, both spectral type and multiplicity. Earlier work produced Lebesgue components, Lebesgue spectrum of higher multiplicity, simple spectrum of other types, flows, or infinite-measure examples; time-$t$ maps of simple-Lebesgue flows have infinite multiplicity, so they do not answer the question. The source also derives from it mixing (of all orders, using a separate companion multiple-mixing theorem), zero Kolmogorov–Sinai entropy (via Rokhlin's finite-multiplicity entropy theorem) and vanishing Lyapunov exponents (Corollary 6.1, p. 28).

Formalizing it. The statement exercises Mathlib's $L^p$ spaces, Haar measure on the additive circle, ergodicity and Fourier characters together. A formal proof would certify a long quantitative construction (successive smooth passages, stationary-phase estimates, Fourier signals) whose convergence must be checked simultaneously in the $C^\infty$ topology and in spectral norms.

Difficulty

Smooth constructions by successive conjugation (Anosov–Katok type) naturally produce maps with singular or discrete spectral behavior, because each approximating map is close to a rotation or an integrable twist with pure point or very structured spectrum. Lebesgue spectral type requires the spectral measure of every function to be absolutely continuous with the right density, and simplicity requires a single orbit to span the whole space. Making both hold in the limit, while keeping the limit map $C^\infty$, requires controlling spectral densities at every scale and approximating every target function by translates of one fixed vector — the step where generic perturbation arguments give no control.

Formalization scope

• The torus is Fin 3 → UnitAddCircle with Measure.pi of AddCircle.haarAddCircle; $T$ is an Equiv.Perm with Smooth T and Smooth T.symm (local $C^\infty$ lifts), and MeasurePreserving T μ μ.
• $L^2_0$ is the complex subspace of Lp ℂ 2 μ with zero integral; $f$ is real-valued almost everywhere. The orbit $v_n=f\circ T^n$ is required to be orthonormal with dense span, i.e. a Hilbert basis indexed by $\mathbb Z$.
• The spectral model is stated with an explicit linear isometric equivalence W : H₀ ≃ₗᵢ[ℂ] CircleH intertwining composition with $T$ and multiplication by fourier 1. Ergodicity is Mathlib's Ergodic T μ.
• Mixing, zero entropy and Lyapunov exponents (Section 6) are not part of the goal.
• Needed infrastructure: stationary-phase estimates, spectral measures of Koopman operators, smooth volume-preserving changes of coordinates on the torus. Spectral-theory infrastructure for Koopman operators is reusable throughout ergodic theory.

Selected references

• V. A. Rokhlin, Selected topics from the metric theory of dynamical systems, Uspekhi Mat. Nauk 4 (1949). https://www.mathnet.ru/eng/rm8607
• S. M. Ulam, A Collection of Mathematical Problems, Interscience Tracts in Pure and Applied Mathematics 8, 1960.
• D. V. Anosov and A. B. Katok, New examples in smooth ergodic theory. Ergodic diffeomorphisms, Trudy Moskov. Mat. Obshch. 23 (1970). https://www.mathnet.ru/eng/mmo237
• H. Helson and W. Parry, Cocycles and spectra, Ark. Mat. 16 (1978). https://doi.org/10.1007/BF02385994
• J. Mathew and M. G. Nadkarni, A measure preserving transformation whose spectrum has Lebesgue component of multiplicity two, Bull. London Math. Soc. 16 (1984). https://doi.org/10.1112/blms/16.4.402
• M. Guenais, Morse cocycles and simple Lebesgue spectrum, Ergodic Theory Dynam. Systems 19 (1999). https://doi.org/10.1017/S0143385799126579
• B. R. Fayad, Partially mixing and locally rank one smooth transformations and flows on the torus $\mathbb T^d$, $d\ge3$, J. London Math. Soc. 64 (2001). https://doi.org/10.1112/S0024610701002447
• A. A. Prikhod'ko, On ergodic flows with simple Lebesgue spectrum, Sb. Math. 211 (2020). https://doi.org/10.1070/SM8147
• B. Fayad, G. Forni and A. Kanigowski, Lebesgue spectrum of countable multiplicity for conservative flows on the torus, J. Amer. Math. Soc. 34 (2021). https://doi.org/10.1090/jams/970
• OpenAI, A smooth three-torus diffeomorphism with simple Lebesgue spectrum, OpenAI Math Release preprint, September 23, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-smooth-three-torus-diffeomorphism-with-simple-Lebesgue-spectrum-September-23-2026/paper.pdf

Motivation

A limit cycle of a planar vector field is a periodic orbit that is isolated among periodic orbits. The second part of Hilbert's sixteenth problem asks how many limit cycles a polynomial vector field of a given degree can have, and it is open even for quadratic fields. The classical Liénard systems

$$\dot x=y-F(x),\qquad \dot y=-x,$$

equivalent to the oscillator equation $x''+F'(x)\,x'+x=0$, are the most studied restricted family. In 1977 Lins, de Melo and Pugh conjectured that for $\deg F=n$ the maximum number of limit cycles is $\lfloor (n-1)/2\rfloor$. The conjecture is now known to fail for $n\ge6$, holds for $n\le4$, and degree five was the remaining undecided case, where it predicts exactly two.

This mission asks for a formal proof of the degree-five bound and its sharpness, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1975 — Rychkov proves the two-cycle bound for odd quintic $F$ (Differ. Uravn. 11, 1975).
• 1977 — Lins, de Melo and Pugh formulate the $\lfloor(n-1)/2\rfloor$ conjecture (LNM 597).
• 2007 — Dumortier, Panazzolo and Roussarie find four cycles with $\deg F=7$ (Proc. AMS 2007).
• 2011 — De Maesschalck and Dumortier find $\lfloor(n-1)/2\rfloor+2$ cycles for every $n\ge6$ (JDE 2011); De Maesschalck and Huzak later obtain at least $n-2$ (JDDE 2015).
• 2012 — Li and Llibre prove at most one limit cycle for $\deg F=4$ (JDE 2012).
• 2014 — Li and Lu bound by two the cyclicity of nondegenerate slow–fast cycles in degree five (JDE 2014), a limiting-regime result.
• 2017 — Llibre and Zhang survey the conjecture (Expo. Math. 2017).
• September 2026 — The OpenAI preprint claims the unrestricted degree-five bound of two (Theorem 1.1, p. 1).

Setting

For a real polynomial $F$ (the primitive of the damping), consider the vector field $V_F(x,y)=(y-F(x),\,-x)$ on $\mathbb R^2$. A solution is a differentiable $z:\mathbb R\to\mathbb R^2$ with $z'(t)=V_F(z(t))$ for all $t$. A periodic orbit is the image of a nonconstant solution that is periodic with some period $T>0$. A limit cycle is a periodic orbit $C$ having an open neighbourhood $U$ such that every periodic orbit contained in $U$ equals $C$. Limit cycles are counted as sets: once each, regardless of multiplicity, stability or hyperbolicity. The periodic orbits of a centre are not limit cycles.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For every real polynomial $F$ with $\deg F\le5$,

$$\#\{C\subset\mathbb R^2:\ C\ \text{is a limit cycle of }V_F\}\ \le\ 2,$$

and some $F$ with $\deg F\le5$ has exactly two limit cycles. No parity, coefficient-sign, hyperbolicity or amplitude restriction is imposed.

Significance

The result itself. It decides the last open degree of the Lins–de Melo–Pugh conjecture in the affirmative, so the conjecture is true exactly for $\deg F\le5$. Unlike the slow–fast result of Li and Lu, it bounds all cycles of every quintic system, including degenerate (multiple) ones and cycles of large amplitude. The preprint also corrects a proposed four-cycle quintic example from the literature by identifying it with a family known to have exactly two periodic solutions (p. 2).

Formalizing it. The statement uses only polynomials, ODE solutions and planar topology, so it is well suited to formal verification, and it would be one of the first machine-checked global limit-cycle bounds for a nonlinear family. The proof's general comparison results for smooth profiles (Propositions 5.2 and 5.3, pp. 32–34) and the global quadratic fit (Theorem 3.6, p. 18) are independent of the polynomial application and reusable.

Difficulty

Small-amplitude (Hopf/Melnikov) calculations only control cycles near the origin or near a perturbation of a centre; they say nothing about distant cycles. The even coefficients of $F$ prevent the reduction to the odd quintic family settled by Rychkov. Generic-perturbation arguments that remove multiple cycles cannot be used, since the count must include degenerate cycles. The preprint keeps the two half-orbits separate, writes each as an arch in coordinates $u=x^2/2$ valid at every amplitude, fits each arch by a quadratic comparison profile (Theorem 3.6), and controls how the fitted parameters move with width through a Schwarzian-type model inequality (Theorem 4.1, p. 20). Periodic orbits then become zeros of a single matching function (Proposition 2.5, p. 10), whose isolated zeros are bounded using an integrating factor (Section 6).

Formalization scope

• The plane is ℝ × ℝ; vectorField F z = (z.2 - F.eval z.1, -z.1) with F : Polynomial ℝ and F.degree ≤ 5 (this includes constants and the zero polynomial, which have no limit cycles).
• IsSolution requires HasDerivAt at every real time; IsPeriodicOrbit asks for a solution, a period T > 0, non-constancy, and C = range z.
• IsLimitCycle F C is a periodic orbit with an open U ⊇ C such that every periodic orbit C' ⊆ U equals C.
• Counting uses Set.encard on the set of limit cycles, so infinitely many would give ⊤; the goal asks for ≤ 2 for every admissible F and = 2 for some.
• Neither conjunct is vacuous: the lower bound requires two actual distinct isolated periodic orbits.

Welcome contributions: existence and smooth dependence of return maps for planar polynomial flows, and the energy-identity first-order return calculation used for sharpness (Section 7, p. 39).

Selected references

• OpenAI, Two limit cycles for quintic Liénard systems, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/two-limit-cycles-for-quintic-lienard-systems-September-24-2026/two-limit-cycles-for-quintic-lienard-systems-September-24-2026.pdf
• A. Lins, W. de Melo, C. C. Pugh, On Liénard's equation, in Geometry and Topology, LNM 597, Springer, 1977, 335–357. https://doi.org/10.1007/BFb0085364
• G. S. Rychkov, The maximal number of limit cycles of the system ẏ=−x, ẋ=y−Σa_i x^{2i+1} is equal to two, Differ. Uravn. 11 (1975), 390–391. https://www.mathnet.ru/eng/de2400
• F. Dumortier, D. Panazzolo, R. Roussarie, More limit cycles than expected in Liénard equations, Proc. AMS 135 (2007). https://doi.org/10.1090/S0002-9939-07-08688-1
• P. De Maesschalck, F. Dumortier, Classical Liénard equations of degree n≥6 can have ⌊(n−1)/2⌋+2 limit cycles, J. Differential Equations 250 (2011). https://doi.org/10.1016/j.jde.2010.12.003
• P. De Maesschalck, R. Huzak, Slow divergence integrals in classical Liénard equations near centers, J. Dyn. Differ. Equ. 27 (2015). https://doi.org/10.1007/s10884-014-9358-1
• C. Li, J. Llibre, Uniqueness of limit cycles for Liénard differential equations of degree four, J. Differential Equations 252 (2012). https://doi.org/10.1016/j.jde.2011.11.002
• C. Li, K. Lu, Slow divergence integral and its application to classical Liénard equations of degree 5, J. Differential Equations 257 (2014). https://doi.org/10.1016/j.jde.2014.08.015
• J. Llibre, X. Zhang, Limit cycles of the classical Liénard differential systems: a survey on the Lins Neto, de Melo and Pugh's conjecture, Expo. Math. 35 (2017). https://doi.org/10.1016/j.exmath.2016.12.001
• K. Odani, Existence of exactly N periodic solutions for Liénard systems, Funkcial. Ekvac. 39 (1996). https://doi.org/10.24546/0100499900

Why paths in the positive orthant matter for networks

A large control system is often built from many subsystems $\Sigma_1,\dots,\Sigma_n$, each of which is input-to-state stable (ISS) with respect to the states of the others. Whether the interconnection is again ISS is decided by a small gain condition on the matrix of interconnection gains. For two subsystems this goes back to Jiang, Teel and Praly (1994) and to the Lyapunov version of Jiang, Mareels and Wang (1996). For $n$ subsystems, Dashkovskiy, Rüffer and Wirth formulated the condition as a property $\Gamma_\mu\not\ge\mathrm{id}$ of a monotone operator on $\mathbb R^n_+$ (2007). Rüffer's thesis (2007) and the paper on which this mission is based (arXiv:0901.1842, SIAM J. Control Optim. 2010) turned it into a Lyapunov construction.

The construction needs a geometric object: a path $\sigma$ in the positive orthant, unbounded in every coordinate, along which the gain operator strictly decreases every component. For a linear gain matrix this is a Perron vector. For nonlinear gains, its existence is the first of the paper's two main results (Theorem 5.2). This mission formalizes that theorem and the lemmas of §8 that prove it. The companion mission formalizes the second main result, the Lyapunov function built from such a path.

Setting

Write $\mathbb R_+=[0,\infty)$. Vectors in $\mathbb R^n_+$ are compared componentwise: $v\le w$ means $v_i\le w_i$ for all $i$, and $v<w$ means $v_i<w_i$ for all $i$. A function $\gamma:\mathbb R_+\to\mathbb R_+$ is of class $\mathcal K$ if it is continuous, strictly increasing and $\gamma(0)=0$, and of class $\mathcal K_\infty$ if it is moreover unbounded.

A gain matrix is $\Gamma=(\gamma_{ij})_{i,j=1}^n$ with $\gamma_{ij}\in\mathcal K\cup\{0\}$ and $\gamma_{ii}\equiv0$. A monotone aggregation function (MAF) is a continuous $\mu:\mathbb R^n_+\to\mathbb R_+$ with $\mu(s)>0$ for $s\ne0$, $\mu(x)<\mu(y)$ whenever $x<y$, and $\mu(x)\to\infty$ as $\|x\|\to\infty$. Typical examples are sums and maxima. Given MAFs $\mu_1,\dots,\mu_n$, the gain operator is

$$\Gamma_\mu(s)_i=\mu_i\big(\gamma_{i1}(s_1),\dots,\gamma_{in}(s_n)\big),\qquad s\in\mathbb R^n_+ .$$

The paper assumes from p. 8 on that $\mu_i$, restricted to the coordinates of the nonzero entries of row $i$, still has the strict monotonicity (Remark 2.6). The small gain condition (SGC) is $\Gamma_\mu\not\ge\mathrm{id}$: for every $s\ne0$, at least one component of $\Gamma_\mu(s)$ is strictly smaller than the corresponding component of $s$. The set

$$\Omega(\Gamma_\mu)=\{s\in\mathbb R^n_+:\Gamma_\mu(s)<s\}$$

collects the points that every component of $\Gamma_\mu$ strictly decreases.

An $\Omega$-path (Definition 5.1) is a continuous $\sigma:\mathbb R_+\to\mathbb R^n_+$ with every component $\sigma_i\in\mathcal K_\infty$ such that (i) each $\sigma_i^{-1}$ is locally Lipschitz on $(0,\infty)$; (ii) on every compact $K\subset(0,\infty)$ the derivatives of all $\sigma_i^{-1}$, where they exist, lie in $[c,C]$ for constants $0<c<C$ depending on $K$ only; and (iii) $\sigma(r)\in\Omega(\Gamma_\mu)$ for all $r>0$.

Formalization targets

Goal: Theorem 5.2

Let $\Gamma$ be a gain matrix and $\mu$ a compatible vector of MAFs. Assume one of: (i) $\Gamma_\mu$ is linear with spectral radius less than one; (ii) $\Gamma$ is irreducible and $\Gamma_\mu\not\ge\mathrm{id}$; (iii) $\mu=\max$ and $\Gamma_\mu\not\ge\mathrm{id}$; (iv) the entries of $\Gamma$ are bounded and $\Gamma_\mu\not\ge\mathrm{id}$. Then

$$\exists\,\sigma\ \text{an }\Omega\text{-path with}\quad\Gamma_\mu(\sigma(r))<\sigma(r)\quad\forall r>0 .$$

In cases (i)–(iii) the entries are in $\mathcal K_\infty\cup\{0\}$, and in case (iv) they are in $(\mathcal K\setminus\mathcal K_\infty)\cup\{0\}$.

Milestones

The milestones follow §8 in the order the proof uses them.

• Bounded gains: Lemmas 8.1–8.3, where iterates of a point of $\Omega$ tend to $0$ and the polygon through them stays in $\Omega$; and Proposition 8.4, which is case (iv).
• Technical lemmas: Lemmas 8.5–8.7 on diagonal operators $\mathrm{diag}(\rho)$ and the decay set $\Psi=\{s:\Gamma_\mu(s)\le s\}$.
• Topological statements: Proposition 8.8, path-connectedness of $\Psi$; Proposition 8.10, where $\Omega$ meets every simplex $S_r=\{s:\sum s_i=r\}$; and Proposition 8.9, where $\Psi_\infty=\bigcap_k\Gamma_\mu^k(\Psi)$ is unbounded.
• Irreducible case: the scaling step quoted from Rüffer's earlier work, and Theorem 8.11, which is case (ii).
• Maximum case: Theorem 8.14, case (iii) in its cycle-condition form.
• Linear case: the Perron step of §8.5, case (i).

Significance

An $\Omega$-path turns a small gain condition into a Lyapunov function. If each $V_i$ is an ISS Lyapunov function of $\Sigma_i$, then $V(x)=\max_i\sigma_i^{-1}(V_i(x_i))$ is one for the network (Theorem 5.3). So Theorem 5.2 is the step that makes the small gain condition a certificate of network stability, and the corollaries of §5–§7 (sums, maxima, neural networks) all pass through it.

The results are published and proved on paper. None is machine-checked: no proof assistant library contains MAFs, gain operators, the sets $\Omega$ and $\Psi$, or $\Omega$-paths. The paper cites three ingredients without proof: Lemma 8.6, Proposition 8.9 and the scaling step of Theorem 8.11. It also gives Theorem 8.14 only as a sketch. Formalizing them closes those gaps in one place.

Difficulty

For bounded gains the problem is easy: far out, every point of a large ray lies in $\Omega$, and the only work is the descent to the origin. With $\mathcal K_\infty$ entries, $\Gamma_\mu$ is unbounded and no ray need stay in $\Omega$. Following the image of a single point fails, because forward iterates go to $0$, not to infinity. The paper instead uses backward orbits inside $\Psi_\infty$. That this set is nonempty and unbounded is a fixed-point argument of Knaster–Kuratowski–Mazurkiewicz type (Propositions 8.9 and 8.10), not a monotonicity argument. A second obstacle is strictness. A backward orbit is only $\le$-increasing, while Definition 5.1 needs strictly increasing components with derivative bounds. This is where the diagonal scalings of Lemmas 8.6–8.7 enter.

Formalization scope

$\mathbb R_+$ is ℝ≥0 and $\mathbb R^n_+$ is Fin n → ℝ≥0, with subsystems indexed from $0$. The strict order $<$ is a named predicate (SLt), never Lean's < on functions, which means "$\le$ and $\ne$". The small gain condition is ∀ s ≠ 0, ¬ s ≤ T s. The inverses $\sigma_i^{-1}$ are carried as explicit two-sided inverses, and derivatives are ordinary real derivatives at points $r>0$ where they exist. Compatibility (Remark 2.6) and $\gamma_{ii}\equiv0$ are hypotheses of every statement about $\Gamma_\mu$. Irreducibility is the matrix-power form of p. 12, which Mathlib's Matrix.isIrreducible_iff_exists_pow_pos connects to Matrix.IsIrreducible. The spectral-radius hypothesis says that every complex eigenvalue has modulus $<1$. The 1-norm defines $S_r$.

Hypotheses made explicit or corrected:

• Theorem 5.2's header types $\Gamma$ in $\mathcal K_\infty\cup\{0\}$ while (iv) needs bounded entries, so each case carries its own entry class.
• Case (iv) is stated as printed, without "no zero rows".
• Proposition 8.10 prints "$T(s)\not\ge s$ for all $s\in\mathbb R^n_+$". No map satisfies this at $s=0$, so it is stated for $s\ne0$.
• Propositions 8.9 and 8.10 assume $n\ge1$.

A path with $\Gamma_\mu(\sigma(r))\le\sigma(r)$, or with Lean's < on functions, is not an $\Omega$-path. Such a reading would make the goal follow from the origin alone, and it is ruled out.

Needed infrastructure: comparison-function calculus (inverses and compositions of $\mathcal K_\infty$ functions), piecewise linear interpolation in $\mathbb R^n_+$ with Lipschitz inverse bounds, and a KKM-type argument on the simplex. The first two are reusable well beyond this mission. Contributions of any milestone, proofs of the cited ingredients (Lemma 8.6, Proposition 8.9, Proposition 8.10, the scaling step of Theorem 8.11) and a full proof of Theorem 8.14 are welcome.

Selected references

• S. N. Dashkovskiy, B. S. Rüffer, F. R. Wirth, Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions, arXiv:0901.1842v2, 2009; SIAM J. Control Optim. 48(6), 2010. https://arxiv.org/abs/0901.1842 , https://doi.org/10.1137/090746483
• S. Dashkovskiy, B. S. Rüffer, F. R. Wirth, An ISS small gain theorem for general networks, Math. Control Signals Systems 19 (2007), pp. 93–122.
• B. S. Rüffer, Monotone dynamical systems, graphs, and stability of large-scale interconnected systems, PhD thesis, Universität Bremen, 2007. http://nbn-resolving.de/urn:nbn:de:gbv:46-diss000109058
• B. S. Rüffer, Monotone inequalities, dynamical systems, and paths in the positive orthant of Euclidean n-space, Positivity, 2009/2010. https://doi.org/10.1007/s11117-009-0016-5
• Z.-P. Jiang, I. M. Y. Mareels, Y. Wang, A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems, Automatica 32 (1996), pp. 1211–1215.

Motivation

Large engineered systems — power grids, chemical plants, logistics and communication networks — are usually modelled as many interacting subsystems. A stability certificate for the whole network is rarely available directly, but each subsystem can often be analysed on its own, treating the states of its neighbours as disturbances. Input-to-state stability (ISS), introduced by Sontag (Sontag 1989), is the robustness notion that makes this decomposition work: it bounds the state by a decaying function of the initial condition plus a gain of the input. A small-gain theorem states that if the gains by which the subsystems influence each other are "small" in a suitable sense, the interconnection is again ISS.

Timeline. Jiang, Teel and Praly proved a nonlinear small-gain theorem for two ISS systems in trajectory form (1994), and Jiang, Mareels and Wang gave its Lyapunov version for two subsystems (1996). Dashkovskiy, Rüffer and Wirth extended the trajectory version to $n$ subsystems with the condition $\Gamma\not\ge\mathrm{id}$ on a nonlinear gain operator (2007). The paper of this mission (arXiv:0901.1842, SIAM J. Control Optim. 48(6), 2010) gives the Lyapunov version for $n$ subsystems with general monotone aggregation of the gains, and constructs the network's ISS Lyapunov function explicitly.

Setting

The network consists of $n\ge 1$ subsystems

$$\Sigma_i:\ \dot x_i=f_i(x_1,\dots,x_n,u),\qquad x_i\in\mathbb R^{N_i},\ u\in\mathbb R^M,$$

with overall state $x=(x_1^T,\dots,x_n^T)^T\in\mathbb R^N$ and dynamics $\dot x=f(x,u)$, $f=(f_1,\dots,f_n)$. $\|\cdot\|$ is the Euclidean norm.

A function $\gamma:\mathbb R_+\to\mathbb R_+$ is of class $\mathcal K$ if it is continuous, strictly increasing and $\gamma(0)=0$, and of class $\mathcal K_\infty$ if moreover unbounded. A positive definite function $\alpha:\mathbb R_+\to\mathbb R_+$ is continuous with $\alpha(r)=0$ only at $r=0$. A Lyapunov function candidate $V:\mathbb R^d\to\mathbb R_+$ is continuous, satisfies $\psi_1(\|x\|)\le V(x)\le\psi_2(\|x\|)$ for some $\psi_1,\psi_2\in\mathcal K_\infty$, and is locally Lipschitz away from the origin.

A candidate $V$ is an ISS Lyapunov function for $\dot x=f(x,u)$ if there are $\gamma\in\mathcal K$ and a positive definite $\alpha$ with

$$V(x)\ge\gamma(\|u\|)\ \Longrightarrow\ \nabla V(x)f(x,u)\le-\alpha(\|x\|)$$

at every point of differentiability of $V$.

On $\mathbb R^n_+$, $v<w$ means $v_i<w_i$ for every $i$. A monotone aggregation function (MAF) $\mu:\mathbb R^m_+\to\mathbb R_+$ is continuous, positive off the origin, strictly increasing for this strict order, and unbounded as $\|s\|\to\infty$. Subsystem $\Sigma_i$ has an ISS Lyapunov function $V_i$ with gains $\gamma_{ij}\in\mathcal K_\infty\cup\{0\}$, $\gamma_{iu}\in\mathcal K\cup\{0\}$ and MAF $\mu_i$ on $\mathbb R^{n+1}_+$ if, wherever $V_i$ is differentiable,

$$V_i(x_i)\ge\mu_i\big(\gamma_{i1}(V_1(x_1)),\dots,\gamma_{in}(V_n(x_n)),\gamma_{iu}(\|u\|)\big)\ \Longrightarrow\ \nabla V_i(x_i)f_i(x,u)\le-\alpha_i(\|x_i\|).$$

The diagonal gains vanish, $\gamma_{ii}\equiv0$. The gain operators are

$$\overline\Gamma_\mu(s,r)_i=\mu_i\big(\gamma_{i1}(s_1),\dots,\gamma_{in}(s_n),\gamma_{iu}(r)\big),\qquad\Gamma_\mu(s)=\overline\Gamma_\mu(s,0).$$

An Ω-path with respect to $\Gamma_\mu$ is a continuous $\sigma:\mathbb R_+\to\mathbb R^n_+$ with every $\sigma_i\in\mathcal K_\infty$, such that each $\sigma_i^{-1}$ is locally Lipschitz on $(0,\infty)$, its derivative lies in $[c,C]$, $0<c<C$, at its points of differentiability in any compact $K\subset(0,\infty)$ (constants depending on $K$ only), and $\Gamma_\mu(\sigma(r))<\sigma(r)$ for all $r>0$.

Formalization targets

Goal: Theorem 5.3

Assume each $V_i$ is an ISS Lyapunov function for $\Sigma_i$ with gains $\Gamma$, $\gamma_{iu}$ and MAFs $\mu_i$; $\sigma$ is an Ω-path with respect to $\Gamma_\mu$; $\varphi\in\mathcal K_\infty$ satisfies

$$\overline\Gamma_\mu(\sigma(r),\varphi(r))<\sigma(r)\qquad\forall r>0;$$

and each $f_i$ is continuous. Then

$$V(x)=\max_{i=1,\dots,n}\sigma_i^{-1}(V_i(x_i))$$

is an ISS Lyapunov function for the network, with gain $\varphi^{-1}$:

$$V(x)\ge\varphi^{-1}(\|u\|)\ \Longrightarrow\ \nabla V(x)f(x,u)\le-\alpha(\|x\|)$$

for a positive definite $\alpha$. The rate $\alpha$ is existential and is not fixed by the statement.

Milestones

The milestones follow the proof on pp. 14–15:

1. $V$ is a Lyapunov function candidate.
2. The maximum rule (5.7) for Clarke generalized gradients.
3. The chain of inequalities showing that the subsystem trigger holds strictly at every active index.
4. The Clarke-gradient form (5.8) of the subsystem decrease.
5. The chain rule for $\sigma_i^{-1}\circ V_i$, with multipliers bounded away from zero.
6. Positivity of the rate: active blocks on a sphere stay away from the origin.
7. The uniform decrease (5.9).

Significance

The result. Theorem 5.3 converts a small-gain condition into an explicit Lyapunov function for the network. Combined with the converse ISS Lyapunov theorem, it gives ISS of the interconnection, and with zero input it gives global asymptotic stability. It covers additive, maximum-type and multiplicative aggregation of gains, and it handles $n$ subsystems without iterating a two-system result. A second main result of the paper (Theorem 5.2, a separate mission) supplies the Ω-path from the condition $\Gamma_\mu\not\ge\mathrm{id}$. Together they reduce the stability of a network to a property of its gain operator.

Formalizing it. The result is proved on paper. As far as we know, no ISS notion, small-gain theorem or monotone aggregation framework has been machine-checked in Lean. This mission produces a Lean statement of the construction, and of its nonsmooth-analysis steps, against which a complete proof can be checked. It also corrects a misprint in the theorem's implication (see Formalization scope).

Difficulty

The function $V$ is a maximum of rescaled functions and is not differentiable on the set where two indices are active, even when every $V_i$ is smooth. The subsystem hypotheses only control derivatives at points where the corresponding $V_i$ is differentiable. At a point where $V$ is differentiable, the active $V_i$ may not be. So the obvious argument — differentiate the active branch and apply (2.7) — fails, and the decrease must be transported through generalized gradients. A second obstacle is uniformity: the rate $\alpha$ must depend on $\|x\|$ alone. This requires the lower derivative bound in the Ω-path definition and a compactness argument on spheres. Dropping the lower bound breaks the theorem, because $\sigma_i^{-1}$ could flatten and remove the decrease.

Formalization scope

Blocks are EuclideanSpace ℝ (Fin (N i)). The network state is the $L^2$ product PiLp 2 (the Euclidean norm, not the sup norm), and the input is EuclideanSpace ℝ (Fin M). Subsystems are indexed by Fin n (0-based) with $n\ge1$. Gains, MAFs, Ω-paths and rates live on ℝ≥0. Lyapunov functions are real-valued with an explicit nonnegativity clause. The strict order on $\mathbb R^n_+$ is a named predicate, not Lean's Pi <. The inverses $\sigma_i^{-1}$ and $\varphi^{-1}$ are explicit arguments with both compositions the identity. Every derivative is guarded by a differentiability hypothesis. Clarke's generalized gradient (2.5) is the published ClarkeGradients.Shared.generalizedGradient on the blocks, and the same definition restated on a general Hilbert space for $\mathbb R^N$ and $\mathbb R$.

Implicit hypotheses made explicit:

• Continuity of every $f_i$. It is the regularity behind the equivalence of the derivative form (2.4) and the Clarke form (2.6) of the decrease condition, which the proof uses.
• $\gamma_{ii}\equiv0$. The paper's convention.
• Compatibility of $\Gamma$ and $\mu$. Remark 2.6, the standing assumption from p. 8 on; it imposes nothing on a zero row of $\Gamma$.

Corrected statement. The printed implication (5.5) has the trigger $V(x)\ge\max_i\varphi^{-1}(\gamma_{iu}(\|u\|))$. With $\overline\Gamma_\mu$ as defined in (2.9), and as the paper's corollaries use it, that implication is false. A counterexample is one subsystem $\dot x=-x+u/6$ with $V_1=|x|$, $\gamma_{1u}(s)=s/10$, $\mu_1(a,b)=a+2b$ and $\sigma=\varphi=\mathrm{id}$, at $x=1$, $u=10$. The proof's chain of inequalities writes $\varphi(r)$ where (2.9) gives $\gamma_{iu}(\varphi(r))$. The goal keeps (2.9) and uses the trigger $V(x)\ge\varphi^{-1}(\|u\|)$, under which the proof closes.

The hypotheses are jointly satisfiable. An example is $n=2$ with $V_i(x_i)=\|x_i\|$, $\mu_i=\max$, $\gamma_{12}=\gamma_{21}=s/4$, $\gamma_{iu}=s/2$, $\sigma(r)=(r,r)$, $\varphi=\mathrm{id}$ and dynamics $f_i=-x_i$. The conclusion is a decrease inequality at the points of differentiability of $V$ for an existential positive definite rate, so it cannot be met by a vacuous choice: $\alpha$ must be positive away from zero. Trajectory-level ISS (Theorem 2.3, cited by the paper) and the corollaries that conclude ISS are out of scope.

Reusable infrastructure: comparison classes, monotone aggregation functions, gain operators and Ω-paths (shared with the Ω-path mission), and the maximum and chain rules for Clarke gradients. Proofs of the nonsmooth calculus milestones are welcome independently of the goal.

Selected references

• S. N. Dashkovskiy, B. S. Rüffer, F. R. Wirth, Small Gain Theorems for Large Scale Systems and Construction of ISS Lyapunov Functions, SIAM J. Control Optim. 48(6), 2010; preprint arXiv:0901.1842v2. https://arxiv.org/abs/0901.1842
• S. Dashkovskiy, B. S. Rüffer, F. R. Wirth, An ISS small gain theorem for general networks, Math. Control Signals Systems 19, 2007. https://doi.org/10.1007/s00498-007-0014-8
• Z.-P. Jiang, A. R. Teel, L. Praly, Small-gain theorem for ISS systems and applications, Math. Control Signals Systems 7, 1994. https://doi.org/10.1007/BF01211469
• Z.-P. Jiang, I. M. Y. Mareels, Y. Wang, A Lyapunov formulation of the nonlinear small-gain theorem for interconnected ISS systems, Automatica 32(8), 1996. https://doi.org/10.1016/0005-1098(96)00051-9
• E. D. Sontag, Smooth stabilization implies coprime factorization, IEEE Trans. Automat. Control 34(4), 1989. https://doi.org/10.1109/9.28018
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309

Motivation

Flexible manufacturing systems are often scheduled by simple distributed rules: each machine looks only at its own buffers and decides, in real time, which part type to work on next. Switching from one part type to another costs a set-up time during which the machine produces nothing, so a natural rule is to work on a buffer until it is empty and only then switch. Perkins and Kumar (IEEE Trans. Automat. Control 34, 1989; reference [18] of the paper) showed that such clearing policies, and in particular clear-a-fraction policies, keep every buffer bounded on acyclic systems whenever each machine has spare capacity. Whether the same holds when material flows around a cycle of machines was left open.

Kumar and Seidman (IEEE TAC 35(3), 1990) answered it negatively by two examples. Example 1 is a single re-entrant part type. Example 2, the subject of this mission, has two part types, neither of which ever revisits a machine, and shows two further phenomena: instability without re-entrance, and the coexistence, for one and the same system, of a bounded periodic regime and an unbounded one, selected only by the initial state.

Setting

A manufacturing system has part types $p$ arriving at rates $d_p$ and machines $m$. Parts of type $p$ follow a fixed route; at stage $i$ they wait in buffer $b_{p,i}$ at machine $\mu_{p,i}$, and processing one of them takes $\tau_{p,i}$. Switching a machine from buffer $b$ to buffer $b'$ takes the set-up time $\delta_{b,b'}$. Flows are continuous: $x_b(t)$ is the level of buffer $b$, $u_b(t)$ and $y_b(t)$ are its cumulative input and output, and

$$x_b(t)=x_b(0)+u_b(t)-y_b(t)\ge 0 .$$

A machine works in runs: a set-up for a buffer, then processing it at rate $1/\tau_b$ while it is nonempty, and at the rate of its inflow while it is empty. A clearing policy (Definition 1) keeps a machine on a buffer $b$ until the first time that $b$ is empty and another of its buffers is nonempty, and then sets it up for one of those. The system is stable if $\sup_{0\le t<\infty}x_b(t)<\infty$ for every buffer $b$.

Example 2 (Fig. 3) has two part types with $d_1=d_2=1$ and two machines. Part type 1 visits buffer 1 at machine 1 and then buffer 2 at machine 2; part type 2 visits buffer 3 at machine 2 and then buffer 4 at machine 1. Processing times are $\tau_1,\dots,\tau_4$ and setting up to buffer $k$ takes $\delta_k>0$. The parameters satisfy the capacity condition (1), $\tau_1+\tau_4<1$ and $\tau_2+\tau_3<1$, and

$$\tau_2+\tau_4>1,\qquad \frac{\delta_1+\delta_4}{1-\tau_1-\tau_4}=\frac{\delta_2+\delta_3}{1-\tau_2-\tau_3}=:\eta,\qquad \delta_4<(1-\tau_3-\tau_4)\eta,\qquad \delta_2<(1-\tau_1-\tau_2)\eta,$$

conditions (7)–(10). The paper's feasible instance is $(\tau_1,\tau_2,\tau_3,\tau_4,\delta_1,\delta_2,\delta_3,\delta_4)=(\tfrac14,\tfrac12,\tfrac14,\tfrac23,\tfrac1{30},\tfrac15,\tfrac1{20},\tfrac1{20})$, with $\eta=1$. For this system there is exactly one clearing policy.

Formalization targets

Goal: stable and unstable modes coexist

For every parameter set satisfying (1) and (7)–(10):

$$\begin{aligned} &\text{from } x(0)=(0,\eta,0,\eta),\ \text{set-ups } (b_1,b_3):\ \text{a clearing trajectory exists, and every one is bounded;}\\ &\exists\,\xi_0\ \forall\,\xi\ge\xi_0,\ \text{from } x(0)=(\xi,0,0,0),\ \text{set-ups } (b_4,b_3):\ \text{a clearing trajectory exists, and every one has } \sup_{t\ge0}x_1(t)=+\infty . \end{aligned}$$

Milestones

1. Case 1, periodic regime: under (1) and (8)–(10), every clearing trajectory from $(0,\eta,0,\eta)$, $(b_1,b_3)$ satisfies $x(\eta)=(0,\eta,0,\eta)$ with the same set-ups.
2. Case 2, Stage 8: under (1) and (7), for large $\xi$, with $t_9=(\xi+\tau_2^{-1}(\delta_1+\delta_2))/(\tau_2^{-1}-1)$: $x(t_9)=(0,0,t_9-\delta_1,0)$, machine 1 set up for buffer 1, machine 2 for buffer 2.
3. Case 2, full cycle: under (1) and (7), for large $\xi$, at an explicit time $t_{17}$, $x(t_{17})=(\lambda\xi+\alpha,0,0,0)$ with set-ups $(b_4,b_3)$, where $\lambda=\tau_2\tau_4/((1-\tau_2)(1-\tau_4))>1$.

Significance

The result shows that stability of a scheduling policy is a property of the initial state as well as of the system: the same parameters admit a bounded periodic orbit and an orbit along which the backlog of buffer 1 is multiplied by $\lambda>1$ in every cycle. The capacity condition (1) holds throughout, so the instability does not come from overload: spare capacity is lost because one machine starves the other. The example also shows that a cycle in the machine graph suffices, without any part type revisiting a machine. Sections IV and V of the paper respond to this by giving a stronger capacity condition under which clear-a-fraction policies are stable, and a supervisory mechanism that stabilizes any policy.

The paper's argument is a stage-by-stage computation of a piecewise-linear trajectory. It has not been machine-checked. A formalization fixes what a clearing trajectory is (including the switching instants at which a buffer is empty but just starting to fill), proves that the trajectories exist and are determined by the initial state, and checks the paper's closed forms. One printed constant is wrong: the offset $\alpha$ of the full cycle lacks a final $-\delta_3$, and the milestone states the corrected value.

Difficulty

The computations within each stage are linear algebra. The difficulty is the event structure. Every stage depends on the order in which the two machines' events occur: whether machine 1 clears buffer 1 before machine 2 has finished its set-ups, whether buffer 2 is still nonempty when buffer 1 empties, and so on. These orderings hold only for $\xi$ large, or only because (8) holds with equality and (9)–(10) hold strictly. The periodic regime depends on exact synchronization. In Case 2, a machine processing an empty buffer at the reduced rate must not be forced off it while its other buffer is empty and not yet fed. A proof must also establish existence of each trajectory, not only compute it.

Formalization scope

• Model. The general system has part types Fin P, machines Fin M, buffers as pairs $(p,i)$ with Lean index $i$ for paper stage $i+1$, real time, and no transport delay or assembly (as in the paper). Example 2 is an instance of this general model, with machines 1, 2 as Lean 0, 1.
• Runs. Each machine follows a sequence of runs. Run 0 is on the initial set-up and has no set-up phase. Run $k\ge1$ has a set-up phase of length $\delta_{\beta_{k-1},\beta_k}$, followed by a processing phase. Runs are never cut during a set-up. If there are infinitely many runs, their start times tend to $\infty$. There is no idling outside runs: a machine serving an empty buffer passes on its inflow.
• Set-up times. They depend only on the target buffer, and $\delta_{b,b}=0$ is never used.
• Processing law. The rate cap is $y_b(t)-y_b(s)\le(1/\tau_b)\cdot$(processing time of $b$ in $[s,t]$). Rate is exactly $1/\tau_b$ while the machine is processing a nonempty buffer.
• Clearing. "Nonempty" in Definition 1 is read as demanding: positive level, or cumulative input strictly increasing from that instant. Under the literal reading the paper's own switching instants would not be "first times", and no clearing trajectory would exist from these initial states. The no-early-exit condition is imposed on the open processing interval.
• Set up for $b$ at $t$. At $t>0$ this refers to the run whose interval $(s_k,s_{k+1}]$ contains $t$.
• Ruling out trivial formalizations. The goal asserts existence of a clearing trajectory in both modes, so neither "every trajectory is bounded" nor "every trajectory is unbounded" can hold vacuously. $\eta$ is computed from the data rather than pinned by hypotheses, and (8) is an equality.

Contributions welcome: existence and uniqueness of clearing trajectories for the two-machine instance, the event-ordering lemmas for large $\xi$, the restart (time-shift) property of trajectories, and the three milestones.

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Transactions on Automatic Control 35(3):289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Transactions on Automatic Control 34:139–148, February 1989 (reference [18] of the paper).

Motivation

A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.

Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.

Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.

Setting

There are $P$ part types and $M$ machines. Part type $p$ arrives at rate $d_p>0$ and follows a route of $n_p$ operations; operation $i$ is done by machine $\mu_{p,i}$ and takes $\tau_{p,i}>0$ per part. Parts awaiting operation $i$ wait in buffer $b_{p,i}$, with level $x_{p,i}(t)\ge 0$. Machine $m$ serves $B_m=\{b_{p,i}:\mu_{p,i}=m\}$, and switching from $b$ to $b'$ costs $\delta_{b,b'}\ge 0$. Flows are continuous: a machine processing a nonempty buffer $b_{p,i}$ drains it at rate $1/\tau_{p,i}$, the output feeds $b_{p,i+1}$ instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.

The load of machine $m$ and the capacity condition are

$$\rho_m:=\sum_{(p,i):\,\mu_{p,i}=m}d_p\tau_{p,i}<1\qquad(1\le m\le M). \tag{1}$$

The system is stable if $\sup_{0\le t<\infty}x_{p,i}(t)<\infty$ for every buffer.

The supervisor picks $\gamma_m$ with

$$\gamma_m(1-\rho_m)>\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b} \tag{24}$$

and thresholds $z_{p,i}\ge0$. It truncates every processing run of $b_{p,i}$ at $\gamma_m d_p\tau_{p,i}$; it keeps a first-come first-served queue $Q_m$ of the buffers that are not being processed and whose level exceeds $z_{p,i}$; when a run ends and $Q_m\ne\emptyset$, the head of $Q_m$ is processed next, for exactly $\gamma_m d_p\tau_{p,i}$ unless it clears earlier. When $Q_m$ is empty the underlying policy is free. Write $\zeta_m:=\gamma_m(1-\rho_m)-\sum_{b\in B_m}\max_{b'\in B_m}\delta_{b',b}>0$ (26) and $\beta_{p,i}(t):=\sum_{j\le i}\tau_{p,i}x_{p,j}(t)$, the backlog of part type $p$ for machine $\mu_{p,i}$.

Formalization targets

Goal: Theorem 2

Under (1), (24) and $z\ge 0$, every supervised trajectory, from every initial state, satisfies

$$\sup_{0\le t<\infty}x_{p,i}(t)<+\infty\qquad\text{for all }p,i.$$

The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.

Milestones: Lemma 1

1. A buffer that enters $Q_m$ at $t_{\rm in}$ completes its next run by $t_{\rm in}+\gamma_m-\zeta_m$ (25).
2. If it enters $Q_m$ with $x_{p,i}(t_{\rm in})\ge\gamma_m d_p$, that run lowers the backlog: $\beta_{p,i}(t_{\rm complete})\le\beta_{p,i}(t_{\rm in})-\zeta_m d_p\tau_{p,i}$.
3. A buffer that enters $Q_m$ at $t_{\rm in}$ and stays above $\max(\gamma_md_p,z_{p,i})$ (strictly above $z_{p,i}$ after $t_{\rm in}$) up to $t'$ has $t'-t_{\rm in}\le(1+\beta_{p,i}(t_{\rm in})/(\zeta_md_p\tau_{p,i}))(\gamma_m-\zeta_m)$.
4. Any interval on which $x_{p,i}\ge g_{p,i}:=\max(\gamma_md_p,z_{p,i})+\gamma_md_p$ has length at most $a_{p,i}+c_{p,i}\beta_{p,i}(t)$.

Significance

The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With $z=0$ it enforces FCFS with truncated runs; with large $z$ and $\gamma$ it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.

The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).

Difficulty

The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine $m$ from upstream machines whose behaviour depends on $m$ itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below $z_{p,i}$; any bound has to account for the time spent below the threshold and for repeated re-entries into $Q_m$, with a set-up paid at each.

Formalization scope

• Model. Part types Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index $i$ is Lean index $i-1$. Time is real with $t\ge0$. Set-up times satisfy $\delta_{b,b}=0$: a set-up is paid only on a switch. No transport delays or assembly, as in the paper.
• Runs. Each machine is always in a run (no idling outside runs); a run is never cut during its set-up; run starts do not accumulate; zero-length runs are allowed. Processing is at rate at most $1/\tau_b$ and only in a processing phase of $b$, and at exactly $1/\tau_b$ while $b$ is nonempty.
• Queue. Membership of $Q_m$ is determined by the trajectory: not on the current run and level strictly above $z_b$. The FCFS key is the start of the current sojourn; ties, including the initial queue at time $0$, are broken arbitrarily, so every initial queue order is covered. A buffer whose run just ended is in $Q_m$ at that instant if its level exceeds $z_b$.
• Lemma 1. Parts 1)–3) assume, as the page does, that the buffer enters $Q_m$ at $t_{\rm in}$. Part 3) adds $x_{p,i}>z_{p,i}$ on $(t_{\rm in},t']$: with the printed non-strict hypothesis the buffer can sit at exactly $z_{p,i}$, never be re-queued, and wait arbitrarily long. In 4), $c_{p,i}$ is $(\gamma_m-\zeta_m)/(\zeta_md_p\tau_{p,i})$.
• Ruled out. The base policy is not restricted to clearing, CAF or any fixed rule, the system is not restricted to few machines or acyclic routes, and the hypothesis of the goal is (24), not $\zeta_m>0$. A non-vacuity witness (one machine, one buffer) shows the class of supervised trajectories is nonempty.
• Reusable. The trajectory model (runs, set-ups, processing law) is the same as in the other missions of this series and applies to any distributed scheduling policy with set-ups.

Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).

Selected references

• P. R. Kumar and T. I. Seidman, Dynamic instabilities and stabilization methods in distributed real-time scheduling of manufacturing systems, IEEE Trans. Automat. Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. R. Perkins and P. R. Kumar, Stable, distributed, real-time scheduling of flexible manufacturing/assembly/disassembly systems, IEEE Trans. Automat. Control 34(2), 139–148, 1989. https://doi.org/10.1109/9.21085