Detailed balanced mass action systems always settle to one equilibrium point
Global Convergence of Detailed Balanced Mass Action Systems
Logic in Computer Science
Summary
The paper solves a key problem in understanding chemical reaction systems where rates follow simple power laws. It shows that in these systems, starting from any positive condition, the system will always settle into one unique steady state. The authors provide a clear and rigorous proof of this fact using a new approach and fully formalize the proof using a computer assistant to ensure correctness. Their method avoids some heavy mathematical tools and checks every step with a proof-checking software.
What this means in practice
- •For chemical process engineers: Guarantee that designed chemical reactors with detailed balanced kinetics will stabilize to a single steady operating point under positive conditions.
- •For systems biologists: Confirm uniqueness and global stability of steady states in biochemical reaction models with detailed balance, aiding model validation and simulation.
A theory result. No direct application yet.
Authors
Haoran Lv, Chengjin Ni, Manqin Wang, Shenli He
Abstract
We give a self-contained proof that, for a finite detailed balanced mass-action system with positive rate constants, each positive stoichiometric compatibility class contains exactly one positive equilibrium and every positive trajectory converges to it, together with a Lean 4 formalization of the complete argument from persistence to convergence. Boundedness and persistence come from the barrier argument of OpenAI (2026) for weakly reversible systems: an arbitrary-tolerance affine approximation yields a finite-minimum barrier whose superlevel sets confine trajectories and give one logarithmic bound for all solutions from a given initial state. The Horn-Jackson dissipation identity identifies the positive equilibria as an exponential family with parameters in the orthogonal complement of the stoichiometric subspace, which gives uniqueness in each class. A bounded-speed descent argument replaces LaSalle's invariance principle; it uses neither uniqueness of solutions nor continuous dependence on initial data, and it places every cluster point in that family. The route given here is direct and elementary, and its main theorem is checked by the Lean kernel against explicit definitions. The proofs, the Lean development, and the manuscript were produced in ClawsGO Science, an agent harness that packages a complete research environment: Claude Opus 5.5 made the research decisions, GPT 6 Astra carried them out, and the Lean kernel checked every formal step.