Proving the existence of localized patterns, periodic solutions, and branches of periodic solutions in the 1D Thomas model
This work provides a rigorous verification method for non-polynomial reaction-diffusion systems, but it is incremental as it applies existing computer-assisted proof techniques to a specific model.
The authors develop a computer-assisted framework to rigorously prove existence of localized patterns, periodic solutions, and branches of periodic solutions in the 1D Thomas model, using a Newton-Kantorovich approach with explicit bounds. The method is demonstrated with code available on GitHub.
In this paper, we present a general framework for constructively proving the existence and of stationary localized solutions, spatially periodic solutions, and branches of spatially periodic solutions in the 1D Thomas model. Specifically, we develop the necessary analysis to compute explicit upper bounds required in a Newton--Kantorovich approach. Given an approximate solution $\bar{\mathbf{u}}$, this approach relies on establishing that a well-chosen fixed point map is contracting on a neighborhood $\bar{\mathbf{u}}$. For this matter, we construct an approximate inverse of the linearization around $\bar{\mathbf{u}}$, and establish sufficient conditions under which the contraction is achieved. This provides a framework for which computer-assisted analysis can be applied to verify the existence and local uniqueness of solutions in a vicinity of $\bar{\mathbf{u}}$, and control the linearization around $\bar{\mathbf{u}}$. Furthermore, as the Thomas model has a non-polynomial nonlinearity, we will need to use different techniques to handle it during our analysis. The code to perform the rigorous proofs is available on Github.