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

TL;DR

This paper introduces a constructive, computer-assisted framework for proving the existence of localized and periodic solutions in the 1D Thomas model, handling non-polynomial nonlinearities.

Contribution

It develops explicit bounds and a fixed point approach for verifying solutions in the Thomas model, including non-polynomial nonlinearities, with code available on GitHub.

Findings

Framework successfully verifies existence of solutions near approximate solutions.

Handles non-polynomial nonlinearities in the Thomas model.

Provides explicit bounds for a Newton--Kantorovich approach.

Abstract

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.