Chemical reaction network species start from zero concentration: there is no laboratory operation that preloads an arbitrary amount of a molecular species into a flask. This rigid starting condition turns out to impose a sharp structural constraint on what a CRN can compute. The constant $0$, surprisingly, is not one of those things — at least not non-trivially.

The Setup

A polynomial initial value problem (PIVP) of dimension $d$ is a system

where $p \colon \mathbb{R}^d \to \mathbb{R}^d$ is a polynomial vector field with rational coefficients. PIVPs are the phase-space model underlying the general-purpose analog computer; each coordinate $y_i(t)$ represents the concentration of a species $X_i$.

The chemical reaction network constraint cuts out a subclass. Reactions are mass-action: any reaction that destroys $X_i$ must list $X_i$ on its left-hand side, because molecules do not disappear without being consumed. At the level of polynomials, this means the field for coordinate $i$ admits a split

where $\mathrm{prod}_i$ (production) and $\mathrm{degr}_i$ (degradation) are polynomials with non-negative rational coefficients. The key structural fact: the degradation is $y_i$ times something non-negative. When $y_i = 0$, the entire degradation term vanishes, leaving only production.

A PIVP with such a decomposition is called CRN-shape. A PIVP is zero-initialized if $y_0 = \mathbf{0}$.

The Question

Consider a one-dimensional example. The scalar ODE $x' = -x$ with $x(0) = 1$ has solution $x(t) = e^{-t} \to 0$. With positive initial data, decay toward $0$ is easy.

Now try to reproduce this with zero initial data. Starting from $x(0) = 0$, the solution is identically $0$: the system never moves.

Can a higher-dimensional, more elaborate CRN achieve the decay that the scalar system cannot? The answer, it turns out, is no. More precisely:

Theorem (Zero-init non-collapse). Let $P$ be a bounded zero-init CRN-shape PIVP. If coordinate $y_i(t_0) > 0$ for some $t_0 \ge 0$, then there exists a constant $c > 0$ such that $y_i(t) \ge c$ holds on a cofinal set of times $t \in [0, \infty)$.

In particular, $\liminf_{t \to \infty} y_i(t) \ge c > 0$, so $y_i(t)$ cannot converge to $0$.

Consequence. If the designated output $y_{i^\ast}$ of a bounded zero-init CRN-shape PIVP converges to $0$, then $y_{i^\ast}(t) = 0$ for every $t \ge 0$. Computing $0$ from zero init is possible only by doing nothing.

Why the Three Hypotheses Matter

Each hypothesis is load-bearing.

• CRN-shape. Without the mass-action decomposition, $x' = -x$, $x(0) = 1$ refutes the conclusion. The CRN constraint forces degradation to vanish at the zero state of the species being degraded.
• Zero init. The same example $x' = -x$ is CRN-shape, but with $x(0) = 1$ rather than $0$, and it has $x(t) \to 0$. Non-zero init lets the system decay.
• Boundedness. Without a bound, an unbounded solution might escape to infinity instead of approaching $0$, but the theorem is really about qualitative behavior in a bounded regime where there is something to say about long-term limits.

Root Species: Where Activity Starts

A CRN starting from $\mathbf{0}$ is, at first, completely inert. For anything to happen, some species must begin to grow. Looking at $p_i(0) = \mathrm{prod}_i(0) - \mathrm{degr}_i(0) \cdot 0 = \mathrm{prod}_i(0)$, the first species to move is one whose production polynomial has a strictly positive constant term. Such species are called roots:

The chemical interpretation is clean: a root is a species produced by an $\emptyset \to X_i$ reaction, i.e., synthesized from nothing at a positive rate.

A non-root species has to be fed, either directly from a root, or via a chain. Formally, root-reachability is the smallest relation such that (i) every root is root-reachable, and (ii) if $\mathrm{prod}_i$ contains a monomial $q_\sigma \prod_j y_j^{\sigma_j}$ with $q_\sigma > 0$ and every active feeder $j$ (i.e., $\sigma_j > 0$) is itself root-reachable, then $i$ is root-reachable.

This is a least-fixed-point definition: start with the roots, iteratively add species fed by already-reached species through a single positive-coefficient monomial, repeat until nothing new is added.

The Proof in Three Moves

Move 1: Non-negativity

The CRN structure preserves non-negativity. If $y_i(t) = 0$ at some instant, then $y_i'(t) = \mathrm{prod}_i(y(t)) \ge 0$ (production polynomial with non-negative coefficients, non-negative feeders). So $y_i$ cannot cross below zero.

Rigorously, one uses a squared-negative-mass Lyapunov functional $V(t) := \sum_i \bigl( \min(y_i(t), 0) \bigr)^2$, which starts at $V(0) = 0$ and satisfies $V' \le L \cdot V$ by local Lipschitzness of the polynomial field on the bounded trajectory ball. Grönwall gives $V \equiv 0$, so $y_i \ge 0$ throughout.

Move 2: Root species have a positive lower bound

For a root $r$ with $c_r := (\mathrm{prod}_r)_0 > 0$, two algebraic facts about non-negative-coefficient polynomials on $\mathbb{R}_{\ge 0}^d$ unlock a scalar Grönwall argument.

• (Lower.) Since $\mathrm{prod}_r(y) = c_r + \text{(non-negative terms)}$, for every $y \ge 0$, $$\mathrm{prod}_r(y) \ge c_r.$$
• (Upper.) On the bounded trajectory ball $\|y\| \le M$, every monomial $y_1^{\sigma_1} \cdots y_d^{\sigma_d}$ is $\le M^{|\sigma|}$ (sum of exponents), so $\mathrm{degr}_r(y) \le D_r$ for an explicit finite constant $D_r$ depending only on the coefficients and $M$.

Combining,

This is a scalar affine inequality in $y_r$. Set $K := D_r + 1 > 0$ (the $+1$ is a cheap regularizer to avoid dividing by zero when $D_r = 0$) and let $\alpha := c_r / K$. The deficit $f(t) := \alpha - y_r(t)$ satisfies $f(0) = \alpha - 0 = \alpha$ and, after a short algebraic rearrangement,

Scalar Grönwall: in the generic case $D_r > 0$,

So $f(t) \le \alpha/2$, i.e., $y_r(t) \ge \alpha/2 > 0$, for all sufficiently large $t$. A positive lower bound is secured. (When $D_r = 0$ the ODE is $y_r' \ge c_r$ and $y_r(t) \ge c_r \cdot t$, which is even better.)

This is where CRN shape really matters: the degradation is linear in $y_r$, which makes the right-hand side of the inequality scalar and affine, which is exactly what Grönwall can digest.

Move 3: Root-reachable species inherit the bound

For non-root species, two things have to happen: show that any positive trajectory must be root-reachable (a graph-theoretic statement), and show that root-reachability propagates the positive lower bound (an analytic statement).

Propagation. Induct on the definition of root-reachability. Base case: roots have a lower bound by Move 2. Step: if $i$ is reached via a monomial $m(y) = q_\sigma \prod_j y_j^{\sigma_j}$ all of whose active feeders $j$ already have positive eventual lower bounds, then $m(y(t))$ has a positive eventual lower bound (product of positive quantities), so $\mathrm{prod}_i(y(t))$ is bounded below by this positive constant beyond some time, and the same scalar Grönwall as in Move 2 gives a lower bound on $y_i$.

Graph traversal (the contrapositive). The deeper half is showing that if $i$ is not root-reachable, then $y_i$ is stuck at zero forever. This is what justifies the “ever positive implies root-reachable” direction that the theorem needs.

The proof uses a quadratic functional on the dead species. Let $R$ be the set of root-reachable species and $N := \{1, \ldots, d\} \setminus R$ be the complement. Define

Three observations:

1. $S(0) = 0$, by zero init.
2. $S(t) \ge 0$ always, as a sum of squares.
3. $S'(t) \le C \cdot S(t)$ for some explicit constant $C \ge 0$.

Given these, scalar Grönwall applied to $S$ yields $S(t) \le 0 \cdot e^{Ct} = 0$ for all $t \ge 0$, hence $S \equiv 0$, hence every $y_j$ with $j \in N$ is identically zero. Any species that ever becomes positive is therefore in $R$.

The content is in observation 3. Differentiating,

The degradation piece contributes $-2 \sum_{j \in N} \mathrm{degr}_j(y(t)) \cdot y_j(t)^2 \le 0$, which we drop. The remaining production piece needs bounding.

Here is the structural claim that makes everything work. For any $j \in N$ and any monomial $\sigma$ of $\mathrm{prod}_j$ with $q_\sigma > 0$, at least one active feeder of $\sigma$ lies in $N$. Because if every active feeder of $\sigma$ lay in $R$, then by the step-clause of the root-reachability definition, $j$ itself would be in $R$, contradicting $j \in N$.

Pick such a dead feeder $k = k(j, \sigma) \in N$. On the bounded ball $\|y\| \le M$,

using $y_\ell \le M$ for the $\ell \ne k, j$ factors and AM–GM for $y_j y_k$. Both $y_j^2$ and $y_k^2$ are summands of $S$. Summing over all $(j, \sigma)$ with positive coefficient produces a uniform bound $S'(t) \le C \cdot S(t)$, and Grönwall closes the argument.

No continuity or first-positive-time analysis is needed: zero init already gives $S(0) = 0$, and Grönwall does the rest.

Combining: if $y_i(t_0) > 0$, then $i$ is root-reachable, so $y_i$ inherits a positive eventual lower bound, which establishes the theorem.

The Lean 4 Formalization

The theorem has been fully mechanized in Lean 4 with Mathlib.

• File: Ripple/Core/ZeroInitPositivity.lean, 1635 lines.
• Main theorem: zero_init_no_collapse (line 1590).
• Consequence: zero_of_limit_is_trivial (line 1610).
• Custom axioms: $0$. The command #print axioms zero_init_no_collapse returns exactly [propext, Classical.choice, Quot.sound], the three standard Mathlib-level axioms.

The formalization took several milestones to complete. The initial scaffold (4ac4c00) stated the theorem modulo three structural axioms. The Step 2 Grönwall argument was discharged in abe1527; the Step 3 analytic propagation in 9c6ab11; the graph-traversal reachability in b1eebc6 (via a rank-form descent on the reachability structure), and the final placeholder everPositive_hasFeedingMonomial in c72484f. Earlier, the local Lipschitz lemma polyPIVP_field_locally_lipschitz was promoted from axiom to theorem in bd1f1e9.

After these commits the proof is axiom-free beyond the three standard Mathlib axioms.

What This Rules Out

The theorem says that any zero-init bounded CRN designed to converge to $0$ must be trivially $0$ throughout. Reading this the other way, it is a structural constraint on the CRN computability of real numbers:

Zero is not a non-trivial CRN-computable number from zero init.

Equivalently, every non-trivial real number computable by a bounded zero-init CRN must be strictly positive: the output cannot come in as a vanishing signal.

The theorem also rules out weaker almost-decays. Could $y_i(t)$ approach $0$ arbitrarily closely without converging to it? No: the cofinal conclusion provides a fixed $c > 0$ that $y_i(t)$ meets or exceeds at arbitrarily large times, which forces $\liminf y_i(t) \ge c$.

Two directions that remain open. The first is quantitative: the explicit $\alpha = c_r / (D_r + 1)$ from Move 2 is provably close to tight, but making the whole bound a computable function of the polynomial data and the ball size $M$ would connect the theorem to the bounded analog complexity hierarchy. The second is structural: the reachability predicate can be decided in polynomial time on the monomial support hypergraph, and understanding how root-reachability composes under common CRN construction operations (dual-railing, cascading) would sharpen the picture considerably.

The full research notes, with theorem statements, complete proofs, and cross-references to the Lean file, are available as PDF.

Nothing comes from nothing; nothing ever could.

— Lucretius, De Rerum Natura, I.155 (after Parmenides)