Global Convergence of Detailed Balanced Mass Action Systems
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.
Related
- Systems genetics identifies ETS1 as a stress-dependent regulator of adipocyte insulin action and heme-iron homeostasis
- Approximating Parameter Regions for Multistationarity and Multistability in Mass-Action Systems
- Toward a global chemogeography of dissolved organic matter: a molecular trait dataset across Earth systems
- Food systems transformation would reshape global agriculture
- Preserving spiking and EEG in detailed models of human cortical microcircuits with morphological reductions
BibTeX
@misc{lv2026global,
title = {{Global Convergence of Detailed Balanced Mass Action Systems}},
author = {Haoran Lv and Chengjin Ni and Manqin Wang and Shenli He},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.30808},
eprint = {2610.30808},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.30808},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Global Convergence of Detailed Balanced Mass Action Systems
AU - Haoran Lv
AU - Chengjin Ni
AU - Manqin Wang
AU - Shenli He
PY - 2026
DA - 2026/10/22
PB - arXiv
DO - 10.48550/arxiv.2610.30808
UR - https://arxiv.org/abs/2610.30808
AB - 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.
ER -