Proving the existence of localized patterns and saddle node bifurcations in 1D activator-inhibitor type models

In this paper, we present a general framework for constructively proving the existence and stability of stationary localized 1D solutions and saddle-node bifurcations in activator--inhibitor systems using computer-assisted proofs. 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, we extend the method to rigorously establish saddle-node bifurcations of localized solutions for the same type of models, by considering a well--chosen zero--finding problem. This depends on the rigorous control of the spectrum of the linearization around the bifurcation point. Finally, we demonstrate the effectiveness of the framework by proving the existence and stability of multiple steady-state patterns in various activator--inhibitor systems, as well as a saddle--node bifurcation in the Glycolysis model.