Ripple now has a formalized continuous-time Markov chain (CTMC) layer and three versions of Kurtz’s mean-field limit theorem, all sorry-free. This post describes what was added and why it matters for the project.

Background

Ripple is a Lean 4 project that formalizes results about chemical reaction network (CRN) computable numbers. The existing codebase covers the deterministic side: polynomial initial value problems (PIVPs/GPACs), dual-rail compilation, large-population protocols, and specific number constructions (e, pi, zeta(3), Catalan’s constant, CM-163).

All of that treats CRNs as continuous dynamical systems. But a real CRN with $N$ molecules is a stochastic process — a continuous-time Markov chain (CTMC) whose state counts how many molecules of each species are present at each moment. The deterministic ODE is what you get in the limit $N \to \infty$, and the theorem that makes this precise is due to Kurtz (1970).

Formalizing this bridge was the next natural step.

What was added

CTMC infrastructure (7 files, ~16K lines)

The new Ripple/CTMC/ directory builds up from discrete-time chains to continuous-time chains to density-dependent processes:

• DTMC.lean — discrete-time Markov chain foundations.
• CTMC.lean — transition rates, holding times, jump chain.
• CTMCProcess.lean — path-level process, jump times, stopped process.
• DensityDependent.lean — the density process $\bar{X}^N(t) = X(t)/N$, where $X$ is the molecule count and $N$ is the system size. This is the largest file (~9.6K lines) and contains the martingale decomposition

where $F$ is the drift and $M^N$ is a martingale with $\mathbb{E}[\sup_{s \le t} \|M^N(s)\|^2] \le C \cdot t / N$.

• RandomIndexDoob.lean — resolves a filtration mismatch that comes up when applying Doob’s $L^2$ inequality at a random index (the jump-count stopping time). The issue is that the natural stopping time is measurable with respect to the shifted filtration $G_n = F_{n+1}$, not the filtration $F_n$ the martingale lives on. The fix defines $\tilde{M}(n) = M(n+1)$ and proves it is a $G$-martingale, then applies Doob $L^2$ to $\tilde{M}$.
• TwoState.lean — two-state birth-death chain with exact stationary distribution.
• CanonicalLaw.lean — probability law of the CTMC process.

Kurtz’s mean-field limit (4 files, ~1.7K lines)

The new Ripple/Kurtz/ directory contains three versions of the theorem, all with zero sorry:

Weak (convergence in probability). For every $\varepsilon > 0$,

where $x(t)$ solves the mean-field ODE $x' = F(x)$. (kurtz_mean_field_convergence)

Strong (almost sure). With probability 1,

(kurtz_strong_approximation)

CLT-scale second moment.

(kurtz_clt_second_moment)

Integral Gronwall inequality

A self-contained lemma (IntegralGronwall.lean): if $u(t) \le \alpha + \int_0^t \beta \cdot u(s)\,ds$ with $\alpha, \beta \ge 0$, then $u(t) \le \alpha \cdot e^{\beta t}$.

The proof defines $v(t) = \alpha + \int_0^t \beta \cdot u(s)\,ds$, applies the fundamental theorem of calculus to get $v'(t) = \beta \cdot u(t) \le \beta \cdot v(t)$, then feeds this into Mathlib’s derivative-form Gronwall (norm_le_gronwallBound_of_norm_deriv_right_le).

How the pieces fit together

The proof chain for the weak Kurtz theorem, for example:

1. The DensityProcess structure provides the martingale decomposition and the quadratic variation bound $\mathbb{E}[\sup \|M^N\|^2] \le C \cdot T / N$.
2. The pathwise Gronwall bound (h_gronwall_pw_of_density_process) turns the integral inequality into $\sup_t \|\text{error}(t)\| \le \sup \|M^N\| \cdot e^{LT}$ for almost every $\omega$, where $L$ is the Lipschitz constant of the drift.
3. Markov’s inequality converts the $L^2$ martingale bound into a probability bound.

The strong version additionally uses Azuma–Hoeffding (measure_sum_ge_le_of_hasCondSubgaussianMGF in Mathlib) and Borel–Cantelli (ae_finite_setOf_mem).

Current status

The full Ripple project builds with lake build (3842 jobs) and has zero sorry and zero axiom declarations across all eight pillars: Core, ODE, DualRail, LPP, Number, Number/Modular, Kurtz, and CTMC.

The one caveat on the trust footprint is unchanged from before: a few native_decide calls in the modular-forms pipeline (CM-163 Sturm bound). These trust the Lean compiler in addition to the kernel.

The code is at github.com/zinan-huang/Ripple.

“One must be able to say at all times — instead of points, straight lines, and planes — tables, chairs, and beer mugs.”

— David Hilbert