Existence and Localization of a Limit Cycle in a Class of Benchmark Biomolecular Oscillators

Oscillatory behaviour is important in multiple biological contexts. However, the inherent nonlinearity and high dimensionality of mathematical models in biology makes proving the existence and the localization of limit cycle oscillations challenging. Here, we provided an elementary proof for the existence and a method for rigorously localizing the oscillatory solutions in a class of benchmark biomolecular oscillators. To construct the proof, we used a geometric approach based on Brouwer Fixed Point theorem. We constructed a toroidal-like manifold within a positively invariant set by removing the hypervolume containing the fixed point and the trajectories converging to it along its stable manifold. We showed that the vector field describing the system dynamics maps a cross section of the toroidal-like manifold onto itself. The existence of a limit cycle solution in this manifold was guaranteed by Brouwer Fixed Point theorem. For different sets of initial conditions in these cross-sections, we used an interval-based Reachability Analysis to localize the oscillatory behaviour that complements the Brouwer Fixed Point theorem approach. These results add a simple and elegant approach to demonstrating the existence of limit cycles in biomolecular systems as well as a method for rigorous localization of the region of existence.