Proving the existence of localized patterns, periodic solutions, and branches of periodic solutions in the 1D Thomas model

In this paper, we present a general framework for constructively proving the existence 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.

Our contributions are to provide a partial answer to how one can approach rigorously verifying results in the Thomas model, to adapt and combine previously developed techniques to apply to the Thomas model, and to perform the computer-assisted analysis to obtain such results.

The code to perform the rigorous proofs is available on Github.