# Classwise permanence for weakly reversible mass-action systems

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Boundedness and persistence of weakly reversible mass-action systems](../../preprints/Boundedness-and-persistence-of-weakly-reversible-mass-action-systems-September-25-2026/paper.pdf)

## Scope

The boundedness and persistence conjectures for mass-action systems ask whether positive concentrations remain finite and separated from zero. The formalization proves this for every finite weakly reversible reaction network with positive constant reaction rates and every strictly positive initial state. A global forward solution exists, and one $\varepsilon\in(0,1)$ bounds every concentration of every global forward solution between $\varepsilon$ and $\varepsilon^{-1}$ for all nonnegative times. The bound may depend on the network, rates, and initial state.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Global boundedness and persistence for weakly reversible mass-action systems | [MassAction.lean](../ComparatorChallenges/MassAction.lean) |