All missions

Motivation

Coordinate descent changes one component of a parameter vector at a time. This matters when evaluating or updating a single component is cheaper than handling the full vector, for example in problems with sparse features. The coordinate chosen at each step can be random or selected from the current gradient. Karimi, Nutini, and Schmidt study these choices for objectives that satisfy a Polyak–Łojasiewicz (PL) inequality, a condition that controls objective error by the size of the gradient without assuming convexity. Their Theorem 3 gives an explicit expected rate for uniform random coordinates, while §3.2 gives a rate for the greedy Gauss–Southwell choice. Karimi, Nutini, and Schmidt (2016), §3

The question is how much of the familiar full-gradient linear rate survives when an update sees only one coordinate. The theorem answers this with a dimension factor: each uniform draw accesses one of $d$ coordinates, and the rate depends on $\mu/(dL)$. The same paper relates the greedy rule to earlier work on coordinate descent and boosting; this mission treats its stated greedy rate as a companion result, using the same coordinate update. Karimi, Nutini, and Schmidt (2016), §§3.1–3.2

Setting

Let $d\ge1$, and let $f:\mathbb R^d\to\mathbb R$ be differentiable. Write $\nabla_i f(x)$ for coordinate $i$ of its gradient and $e_i$ for the corresponding standard basis vector. The paper's coordinate-wise upper bound (5), with $L>0$, is

$$f(x+\alpha e_i)\le f(x)+\alpha\nabla_i f(x)+\frac L2\alpha^2 \quad\text{for every }x\in\mathbb R^d,\ i\in\{1,\ldots,d\},\ \alpha\in\mathbb R.$$

Here $i$ ranges over the $d$ coordinates. The bound concerns motion along one coordinate. It is the exact smoothness condition used in Theorem 3. Let $x^*$ be a global minimizer and put $f^*=f(x^*)$; thus the solution set is nonempty and $f^*$ is an attained optimal value. The PL inequality (3) with $\mu>0$ says

$$\frac12\|\nabla f(x)\|^2\ge\mu\bigl(f(x)-f^*\bigr) \quad\text{for every }x\in\mathbb R^d.$$

The randomized coordinate-descent step (6) draws $i_k$ uniformly from the $d$ coordinates, independently at each time, and sets $x_{k+1}=x_k-L^{-1}\nabla_{i_k}f(x_k)e_{i_k}$. The initial point $x_0$ is arbitrary. For $k$ draws, expectation means the average over all $d^k$ words $(i_0,\ldots,i_{k-1})$, each assigned weight $d^{-k}$. In particular, at $k=0$ the empty word has weight one and the iterate is $x_0$.

The Gauss–Southwell rule instead chooses a coordinate with the largest $|\nabla_i f(x_k)|$; ties may be resolved in any way. Its rate uses a PL inequality in the maximum-coordinate norm, $\|\nabla f(x)\|_\infty=\max_i|\nabla_i f(x)|$, with constant $\mu_1>0$. Karimi, Nutini, and Schmidt (2016), pp. 5–6

Formalization targets

Theorem 3: uniform random coordinates

For every $k\ge0$, the goal is the paper's expected suboptimality bound

$$\mathbb E[f(x_k)-f^*] \le\left(1-\frac{\mu}{dL}\right)^k\bigl(f(x_0)-f^*\bigr).$$

The target includes the specific update (6), the coordinate condition (5), and the PL inequality (3). The three milestones are the paper's displayed one-coordinate decrease, its uniform expected decrease involving $\|\nabla f(x)\|^2$, and the resulting conditional expected gap contraction. They are indexed to the proof of Theorem 3 on page 5. Karimi, Nutini, and Schmidt (2016), Theorem 3 and proof

Greedy coordinate choice

The companion target is the rate stated in §3.2 when the maximum-norm PL inequality holds:

$$f(x_k)-f^* \le\left(1-\frac{\mu_1}{L}\right)^k\bigl(f(x_0)-f^*\bigr).$$

This bound applies to any run that chooses a maximizing coordinate at every step. The different PL modulus is part of the statement; it need not equal the modulus $\mu$ in Theorem 3. Karimi, Nutini, and Schmidt (2016), §3.2

Significance

Theorem 3 gives a quantitative guarantee for a method that reads one gradient component per update. The guarantee depends on the attained optimum, the coordinate smoothness constant, the PL modulus, and the number of coordinates. It applies to objectives satisfying PL even when convexity is unavailable. The companion result records how the stated rate changes when the coordinate is selected by the largest gradient component and the PL condition is measured in the corresponding dual norm. Karimi, Nutini, and Schmidt (2016), §3

The paper proves these claims, but this mission asks for machine-checked proofs of their exact hypotheses and constants. A complete development will make the finite random experiment explicit and give reusable definitions for coordinate updates and expectations of finite coordinate-choice histories. The PL predicate is already published in the theorem library; the coordinate model and the results here remain to be formalized.

Difficulty

A bound for a single coordinate update depends on one component of the gradient. An arbitrary coordinate can have a zero component even when the full gradient is large, so a pointwise decrease with the full gradient norm cannot be asserted for every choice. The theorem instead concerns the expectation over a uniform choice and then over the complete history of choices. The main formal difficulty is keeping those two levels of expectation aligned with a state $x_k$ that itself depends on earlier draws. For the greedy companion, the selected coordinate may not be unique; the statement must cover every maximizing choice without assuming a fixed tie-breaking rule.

Formalization scope

The vector space is EuclideanSpace ℝ (Fin d). The shared definitions give (5), the step (6), the iterate produced by a word Fin k → Fin d, and the expected gap as a real finite sum. The published ShiOptRates.PolyakLojasiewicz predicate represents (3) after multiplying both sides by two. Every theorem using uniform draws assumes $d>0$; every step with $1/L$ assumes $L>0$. The goal also states differentiability, an explicit global minimizer, and $\mu>0$. No convexity is assumed. A free real number called $f^*$ would change the PL condition and could invalidate the rate, so the formal statement uses $f(x^*)$ throughout.

The index-word average is an exact finite representation of independent uniform sampling, including $k=0$. It does not sample coordinates without replacement. The companion theorem represents the maximum-norm PL condition by requiring its inequality at every maximizing coordinate, which is equivalent for $d>0$, and quantifies over every run satisfying the Gauss–Southwell update relation. Useful contributions include proofs of the three displayed milestones, the passage from one draw to the word average, and the greedy companion. The paper's optional remark on sampling proportional to coordinate-specific constants $L_i$ and its exact-coordinate-minimization remark are outside this proposal.

Selected references

• H. Karimi, J. Nutini, and M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD, 2016; arXiv:1608.04636v4.

Motivation

An assortment decision determines which products a seller makes available to a customer. When customers differ, the seller may first choose a limited collection of products and then decide which of those products to display to each arriving customer. This is a concrete way to represent personalized product pages or offers with a common inventory or display budget. The benefit of that second decision is not immediate from a single-customer model: personalization can remove products that dilute one type's purchases while retaining them for another type. El Housni and Topaloglu quantify this benefit for a mixture of multinomial logit choice models.

Their Theorem 3.1 compares optimal expected revenue with and without customer-type customization. It gives a universal factor depending only on the number of types and an explicit family showing that this order can occur. The result is already proved in the authors' SSRN version of December 7, 2021. This mission concerns the statements and proof in that version; the published Operations Research article appeared in 2023 and may use different numbering.

Setting

There are $n$ products $N=\{1,\ldots,n\}$ and $m$ customer types $M=\{1,\ldots,m\}$. Product $i$ earns revenue $r_i>0$ when purchased. Customer type $j$ arrives with probability $\theta_j\ge0$, with $\sum_{j\in M}\theta_j=1$. Its preference weight for product $i$ is $v_{ij}\ge0$; the no-purchase alternative has weight one. An assortment $S\subseteq N$ offered to type $j$ yields MNL expected revenue

$$\operatorname{Rev}_j(S)=\frac{\sum_{i\in S}r_i v_{ij}}{1+\sum_{i\in S}v_{ij}}.$$

The seller may initially carry at most $K$ products. In the customized assortment problem (CAP), it chooses $S$ and, after seeing the type, offers a subset $S_j\subseteq S$. For a fixed carried set, write $f_j(S)=\max_{T\subseteq S}\operatorname{Rev}_j(T)$ and $f^C(S)=\sum_{j\in C}\theta_j f_j(S)$ for any collection $C$ of types. Thus $f^M(S)$ is the expected personalized revenue. In the mixed multinomial logit problem (MMNL), the same carried assortment $S$ is offered to every type. Both models obey the same first-stage cardinality limit:

$$z_{\rm CAP}=\max_{S\subseteq N,\ |S|\le K}f^M(S),\qquad z_{\rm MMNL}=\max_{S\subseteq N,\ |S|\le K}\sum_{j\in M}\theta_j\operatorname{Rev}_j(S).$$

This formulation follows §2 and §3 of the December 2021 SSRN version, pp. 5–7. A zero preference weight is allowed: the authors' tightness instance assigns zero to products a type does not consider.

Formalization targets

Theorem 3.1: universal comparison

For every valid model and every first-stage budget $K$, the target is

$$z_{\rm MMNL}\le z_{\rm CAP}\le m\,z_{\rm MMNL}.$$

The factor counts customer types, not products. The result covers $K=0$ as well: both values are zero. It does not assume the products are sorted by revenue, since the numerical indexing convention in §2 is unnecessary for this comparison and is incompatible with the paper's tightness family.

Theorem 3.1: order-tight family

The same theorem says that there are instances for which the CAP value is $\Omega(m)$ times the MMNL value. The formal target uses the instance constructed in its proof, pp. 8–9 and records the explicit bound implied there:

$$z_{\rm MMNL}>0,\qquad z_{\rm CAP}\ge\frac{m}{6}\,z_{\rm MMNL}\qquad(m\ge2).$$

In this family $n=K=m$. With $\alpha=(\sum_{j=1}^m a^{-j})^{-1}$, the parameters are $\theta_j=\alpha/a^j$, $r_i=a^i$, and $v_{ij}=b^{m-i+1}$ when $i\le j$ and zero otherwise. The proof chooses $b=m-1$ and $a=2m(m-1)^m$. The goal also asserts that this family satisfies the model assumptions. The accompanying milestones are the paper's typewise comparison, the CAP lower bound, equation (3.1), its two term bounds, and the MMNL upper bound.

Significance

The universal inequality limits the improvement that type-specific displays can offer in this model using only the number of types. The family in the second part shows that no bound independent of $m$ can replace it across all valid instances. Thus the comparison locates the possible value of customization even when the seller may carry every product. It also distinguishes the effect of a shared display from the effect of the common product budget, since the example has $K=n$.

The paper already proves both claims. A complete formal development would check the exact MNL revenue formula, the two finite optimization problems, and the asymptotic example within one Lean environment. It would leave reusable definitions for personalized and common assortments under a mixture of choice models. The statements in this draft compile with proof placeholders; this mission does not claim that the theorem has a machine-checked proof yet. It welcomes proofs of the listed milestones, lemmas about finite maxima and nonnegative MNL revenue, and a proof of the combined goal.

Difficulty

For each type, personalization maximizes revenue over its own subset of $S$; MMNL must use one subset for all types. Exchanging the sum over types with a maximum over assortments would erase that distinction and is generally invalid. A simple comparison of the two optima gives the first inequality but cannot explain the precise factor $m$ or why it can be approached in order. The tightness family also balances rapidly changing revenues and arrival probabilities against preference weights. Its boundary case $m=2$ has $b=1$, so a claim needing $b>1$ would miss a valid member of the family.

Formalization scope

Lean represents products by Fin n, customer types by Fin m, and assortments by Finset (Fin n). The paper's one-based product $i$ is Lean's index i.val + 1: $a^i$ becomes a ^ (i.val + 1), and $b^{m-i+1}$ becomes b ^ (m - i.val). The preference function takes product first and type second, matching $v_{ij}$. The common revenue calculation imports the published ChoiceCDLP.MNL.mnlObjective with no-purchase weight one.

All maxima are Finset.sup' over nonempty finite families. The feasible family contains the empty assortment for every natural-number budget; the personal subassortment family contains the empty set as well. This makes the values genuine finite maxima, including at zero budget. No real sSup fallback value is used. The standing assumptions are positive revenues, nonnegative preference weights, nonnegative arrival probabilities, and a probability sum of one. The explicit instance is restricted to $m\ge2$, has positive MMNL value, and satisfies each standing assumption. These conditions exclude a vacuous $\Omega(m)$ ratio based on zero MMNL value or an instance outside the model.

The complete development needs elementary facts about finite sums, powers, ordered Finsets, finite maxima, and nonnegative rational functions. The MNL objective is already a separate published definition; the paper-specific CAP, MMNL, and instance definitions are local. The proof targets are the claims printed in the December 2021 SSRN version, with the constant $1/6$ disclosed as an explicit pin from its proof.

Selected references

• O. El Housni and H. Topaloglu, Joint Assortment Optimization and Customization under a Mixture of Multinomial Logit Models: Value of Personalized Assortments, SSRN 3830082, version of December 7, 2021, §§2–3, pp. 5–9; published in Operations Research, 2023. SSRN

Motivation

Gradient descent on a smooth function $f:\mathbb R^d\to\mathbb R$ converges at a linear rate (the optimality gap shrinks by a constant factor each step) under strong convexity. Many problems in machine learning and statistics are not strongly convex: least squares with a rank-deficient design, logistic regression on separable or degenerate data, and some non-convex objectives. Over roughly 25 years several weaker conditions were proposed that still give linear convergence. Examples are the error bound of Luo and Tseng, restricted strong convexity, essential strong convexity, weak strong convexity, and quadratic growth (also called optimal or semi-strong convexity). Each came with its own proof, usually assuming convexity. How these conditions relate to one another was rarely made explicit.

Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) put the Polyak–Łojasiewicz (PL) inequality (Polyak, 1963) at the centre. Their Theorem 2 orders seven conditions by strength for functions with a Lipschitz gradient, without convexity. It shows that PL is equivalent to the error bound and implies quadratic growth. For convex functions it shows that the four weakest conditions coincide. The equivalence of EB and PL is a special case of a result of Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234, Theorem 5). Zhang (arXiv:1606.00269) independently related RSI, EB, PL and QG.

Setting

Let $f:\mathbb R^d\to\mathbb R$ be differentiable with gradient $\nabla f$. The paper's standing assumptions (§2, p. 2) are:

1. $\nabla f$ is $L$-Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$, with $L>0$;
2. the solution set $\mathcal X^*=\{x:\ f(x)\le f(y)\ \forall y\}$ is non-empty. Write $f^*$ for the optimal value.

For every $x$, $x_p$ denotes a projection of $x$ onto $\mathcal X^*$: a point of $\mathcal X^*$ at distance $\operatorname{dist}(x,\mathcal X^*)$ from $x$. Each of the following conditions involves a constant $\mu>0$, which may differ between conditions (Appendix A, pp. 11–12):

• SC (strong convexity): $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2$ for all $x,y$.
• ESC (essential strong convexity): the same inequality for all $x,y$ with $x_p=y_p$.
• WSC (weak strong convexity): $f^*\ge f(x)+\langle\nabla f(x),x_p-x\rangle+\frac\mu2\|x_p-x\|^2$ for all $x$.
• RSI (restricted secant inequality): $\langle\nabla f(x),x-x_p\rangle\ge\mu\|x_p-x\|^2$ for all $x$.
• EB (error bound): $\|\nabla f(x)\|\ge\mu\|x_p-x\|$ for all $x$.
• PL (Polyak–Łojasiewicz): $\frac12\|\nabla f(x)\|^2\ge\mu(f(x)-f^*)$ for all $x$.
• QG (quadratic growth): $f(x)-f^*\ge\frac\mu2\|x_p-x\|^2$ for all $x$.

Formalization targets

Goal: Theorem 2 (p. 3)

Read each condition as "it holds for some $\mu>0$". For $f$ with a Lipschitz-continuous gradient,

$$(SC)\to(ESC)\to(WSC)\to(RSI)\to(EB)\equiv(PL)\to(QG),$$

and if $f$ is also convex,

$$(RSI)\equiv(EB)\equiv(PL)\equiv(QG).$$

The goal states no constants, because the constant may change along the chain.

Milestones: the implications of Appendix A, with their constants

The appendix proves a subset of the arrows, each with an explicit constant. The rest follow by transitivity.

$$\text{SC}(\mu)\Rightarrow\text{ESC}(\mu),\quad \text{ESC}(\mu)\Rightarrow\text{WSC}(\mu),\quad \text{WSC}(\mu)\Rightarrow\text{RSI}(\mu/2),\quad \text{RSI}(\mu)\Rightarrow\text{EB}(\mu),$$ $$\text{EB}(\mu)\Rightarrow\text{PL}(\mu^2/L),\quad \text{PL}(\mu)\Rightarrow\text{QG}(\mu),\quad \text{PL}(\mu)\Rightarrow\text{EB}(\mu),\quad \text{QG}(\mu)+\text{convex}\Rightarrow\text{RSI}(\mu/2).$$

One further milestone is display (20). Under PL, $g=\sqrt{f-f^*}$ satisfies $\|\nabla g(x)\|\ge\sqrt{\mu/2}$ at every $x\notin\mathcal X^*$.

Significance

The result. Theorem 2 shows that QG is the weakest of the seven conditions. QG alone does not rule out non-global local minima, so it cannot guarantee that gradient descent reaches a global minimizer. Among the conditions considered, PL and the equivalent EB are therefore the most general that still give linear convergence to a global minimum. The paper's Theorem 1 gives that rate under PL with a one-paragraph proof. For convex $f$, RSI (there called restricted strong convexity), EB, PL and QG are one condition. A rate proved under any of them transfers to the others, up to the constants of the milestones.

Formalizing it. The result is proved on paper, and the arrows of Appendix A are short, except PL → QG. A machine-checked version adds three things. It fixes a precise meaning for $x_p$ when $\mathcal X^*$ is not convex and a nearest point is not unique. It records the correct constant in EB → PL: the printed text says $\mu/L$, while the displayed argument yields $\mu^2/L$. It puts PL → QG for non-convex $f$ on a checked footing; the acknowledgments note an earlier error in this proof. No formalization of these implications is known to be on the platform or in Mathlib.

Difficulty

Most arrows are one-line rearrangements or the Cauchy–Schwarz inequality. EB → PL also needs the quadratic upper bound implied by the Lipschitz gradient, and $\nabla f(x_p)=0$ at a global minimizer.

The obstacle is PL → QG without convexity. The natural first idea fails. Integrating along the segment from $x$ to $x_p$ uses no information from PL, because the gradient along that segment is unrelated to the gap $f-f^*$. The implication is global: it converts a pointwise bound on the gradient into a lower bound on $f$ in terms of the distance to a possibly non-convex set $\mathcal X^*$. Any proof has to bound the distance to $\mathcal X^*$ by the length of some path into it that is controlled by $f$. Building such a path in Lean, with its existence, its arrival at $\mathcal X^*$ in finite time and a bound on its length, needs analysis that is not yet assembled in Mathlib for this purpose.

Formalization scope

• Space. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), abbreviated E d. Gradients are Mathlib's gradient. The Lipschitz gradient is the literal hypothesis ∀ x y, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖ with 0 < L, together with Differentiable ℝ f.
• Solution set. Non-emptiness is carried by a global minimizer xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar. In WSC, $f^*$ is written $f(x_p)$.
• Projection. $x_p$ is an explicit map p with IsProjSel f p: p x lies in $\mathcal X^*$ and ‖x - p x‖ = Metric.infDist x X*. Every condition, and Theorem 2, refers to an arbitrary such selection. ESC's "$x_p=y_p$" is p x = p y for that same selection. No Classical.choose is used.
• PL is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ fstar (definition ShiOptrates_FunctionClass), i.e. $2\mu(f(x)-f^*)\le\|\nabla f(x)\|^2$. This is the paper's (3) multiplied by 2.
• Constants. Each milestone carries the constant of its appendix bullet and the hypothesis $\mu>0$. The goal uses Holds C := ∃ μ, 0 < μ ∧ C μ independently on each side of every arrow. Convexity is ConvexOn ℝ Set.univ f.
• Dropped standing hypotheses. Milestones whose argument does not use the Lipschitz gradient omit it: SC → ESC, ESC → WSC, WSC → RSI, RSI → EB, QG + convex → RSI, and (20). Each is then a slightly stronger statement.
• Corrected constant. EB → PL is stated with $\mu^2/L$, which is what the paper's displayed argument proves. The quoted milestone text keeps the printed "$\mu/L$".
• No trivialization. Every condition is quantified over all $x$ (and $y$). The selection p is constrained by IsProjSel, not free, and the goal's hypotheses are satisfiable: $f(x)=\frac12\|x\|^2$ with $p\equiv0$, $L=1$ satisfies all of them and SC with $\mu=1$. A formalization that fixed one $\mu$ for the whole chain, or replaced $x_p$ by an unconstrained map, would be a different theorem.
• Reuse. The condition predicates and the projection selection are reusable by any development on linear convergence without strong convexity. A general "PL implies QG" lemma via gradient flow is reusable beyond this mission. Contributions toward the ODE and arc-length infrastructure are welcome.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4 (2020). https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, Zh. Vychisl. Mat. Mat. Fiz. 3(4):643–653, 1963 (English translation: USSR Comput. Math. Math. Phys. 3(4):864–878). https://doi.org/10.1016/0041-5553(63)90382-3
• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165, 2017. https://arxiv.org/abs/1510.08234
• H. Zhang, The restricted strong convexity revisited: analysis of equivalence to error bound and quadratic growth, Optim. Lett. 11, 2017. https://arxiv.org/abs/1511.01635
• H. Zhang, New analysis of linear convergence of gradient-type methods via unifying error bound conditions, Math. Program. 180, 2020. https://arxiv.org/abs/1606.00269
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46, 1993. https://doi.org/10.1007/BF02096261

Motivation

A high dimensional expander is a simplicial complex whose local structure forces global expansion. The high order random walks on such a complex move from a $k$-face to a $k$-face through a common $(k+1)$-face. They were studied for their connection to agreement tests in probabilistically checkable proofs (Dinur–Kaufman 2017; Kaufman–Mass 2017), and they later became a tool for sampling. Anari, Liu, Oveis Gharan and Vinzant (arXiv:1811.01816) used the mixing bound of this mission to prove the Mihail–Vazirani conjecture: the bases-exchange walk of every matroid mixes rapidly.

Timeline:

• 1973. Garland (Ann. of Math. 97) shows that spectral gaps in the links of a complex control its cohomology. Inner products are localized to links; this is now called Garland's method.
• 2017. Kaufman and Mass (arXiv:1604.02947) bound the second eigenvalue of the high order walks on complexes with well-expanding links. Dinur and Kaufman obtain the optimal bound under a two-sided spectral gap in the links, as Kaufman–Oppenheim explain.
• 2018. Oppenheim (Discrete Comput. Geom. 59) shows how spectral gaps descend from top-dimensional links to lower ones ("trickling down").
• 2017–2021. Kaufman and Oppenheim (arXiv:1707.02799v3) obtain the optimal mixing bound under a one-sided gap only: negative eigenvalues of the links do not matter. This is the target of this mission.

Setting

Let $V$ be a type of vertices. A pure $n$-dimensional finite simplicial complex $X$ is a finite family of finite subsets of $V$ that is closed under subsets, has faces of at most $n+1$ elements, and has every face contained in a face of exactly $n+1$ elements. A face with $k+1$ elements is a $k$-face; $X(k)$ is the set of $k$-faces, and $X(-1)=\{\emptyset\}$.

A weight function is a map $m$ from the faces of $X$ to $(0,\infty)$ that is balanced: for $-1\le k\le n-1$ and $\tau\in X(k)$,

$$m(\tau)=\sum_{\sigma\in X(k+1),\ \tau\subseteq\sigma}m(\sigma).$$

A $k$-cochain is a function $\phi:X(k)\to\mathbb R$. The cochains carry the inner product $\langle\phi,\psi\rangle=\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)\psi(\sigma)$ and the norm $\|\cdot\|$. The cochains orthogonal to the constants form $C^k_0(X,\mathbb R)=\{\phi:\sum_{\sigma\in X(k)}m(\sigma)\phi(\sigma)=0\}$.

The upper random walk $M^+_k$ acts on $k$-cochains by

$$M^+_k\phi(\tau)=\frac{1}{k+2}\,\phi(\tau)+\sum_{\tau'\in X(k),\ \tau\cup\tau'\in X(k+1)}\frac{m(\tau\cup\tau')}{(k+2)\,m(\tau)}\,\phi(\tau').$$

It stays put with probability $1/(k+2)$, and otherwise moves to a neighbouring $k$-face with probability proportional to the weight of their union.

The link of a face $\tau$ is $X_\tau=\{\eta\in X:\eta\cap\tau=\emptyset,\ \tau\cup\eta\in X\}$, weighted by $m_\tau(\eta)=m(\tau\cup\eta)$. On the vertices of $X_\tau$, the non-lazy upper walk $(M')^+_{\tau,0}=2M^+_{\tau,0}-I$ is the weighted random walk on the 1-skeleton of the link. Let $\mu_\tau$ be its second largest eigenvalue. $X$ is a one-sided $\lambda$-local spectral expander if $\mu_\tau\le\lambda$ for every face $\tau$ of dimension $-1,\dots,n-2$. The empty face is included, and its link is $X$ itself.

Formalization targets

Goal: Theorem 5.4 (p. 17)

Let $0\le\lambda\le1$ and let $X$ be a one-sided $\lambda$-local spectral expander. Then for every $0\le k\le n-1$ and every $\phi\in C^k_0(X,\mathbb R)$,

$$\|M^+_k\phi\|\le\Big(\frac{k+1}{k+2}+\frac{k+1}{2}\,\lambda\Big)\|\phi\|.$$

Milestones

They follow the paper's proof order:

• Lemma 3.6 and Corollary 3.7: the adjoint $d^*$ of the signless differential $d$, and the factorizations $d^*d=(k+2)M^+_k$, $dd^*=(k+1)M^-_k$.
• Proposition 4.1 (1)–(3), Garland's localization identities, and Proposition 4.2:

$$\|d\phi\|^2=\|d^*\phi\|^2+\|\phi\|^2+\sum_{\tau\in X(k-1)}\langle (M')^+_{\tau,0}(I-M^-_{\tau,0})\phi_\tau,\phi_\tau\rangle .$$

• Lemma 4.3, which bounds the link terms by $(k+1)\mu\|\phi\|^2$.
• Lemma 5.1.
• Theorem 5.2 (the Decomposition Theorem).
• Corollary 5.3, in its general and its one-sided form:

$$\|d\phi\|^2\le\sum_{j=0}^{k}\Big(k+1-j+\frac{(k+j+2)(k+1-j)}{2}\lambda\Big)\|\phi^j\|^2,\qquad \|\phi\|^2=\sum_{j=0}^k\|\phi^j\|^2.$$

Significance

The result. The coefficient $\frac{k+1}{k+2}$ is the baseline in the paper's mixing bound, and the bound is optimal up to the $O(\lambda)$ term. It needs a gap on one side only: links may have eigenvalues near $-1$. This matters in two places. The links of a matroid's independence complex are only one-sided expanders, so the matroid application needs exactly this case. And the links of Ramanujan complexes are one-sided expanders, so this bound gives optimal mixing on them; the two-sided bound of Dinur–Kaufman does not apply to them.

Formalizing it. The theorem is proved on paper; the Lean statements in this mission are proof targets. Completing the mission would give machine-checked proofs of the mixing bound, Garland's localization identities, and the Decomposition Theorem, built on definitions of weighted simplicial complexes, links, and their random walks. Lemma 4.3 and Corollary 5.3 are stated with a correction: as printed they are false when a link eigenvalue bound is negative (see Formalization scope).

Difficulty

The obvious argument fails. The tempting route bounds the second eigenvalue of $M^+_k$ directly from the link spectra, by induction on $k$. But $M^+_k$ has large eigenvalues near $\frac{k+1-j}{k+2}$ for every $j$, coming from cochains of the form $d\psi$ with $\psi$ of lower degree. A single spectral-gap estimate cannot separate these levels from one another. The paper instead splits $\phi$ into contributions from every degree $j\le k$; this is the Decomposition Theorem, and each piece is controlled separately. Formally, the main costs are:

• the double-counting behind Proposition 4.1 (Appendix A, pp. 28–29);
• a square root of a positive self-adjoint operator on a weighted finite-dimensional space (Theorem 5.2);
• the bookkeeping of degrees and links.

Formalization scope

Faces are Finset V. $X$ is a Finset (Finset V), and $X(k)$ is cells X (k + 1): faces are indexed by their number of vertices. Cochains are functions Finset V → ℝ that are read only on the relevant faces. Every operator is zero off $X$. The weight is positive on faces; the paper writes $\mathbb R^+$, and $m$ appears in denominators. Every goal-level statement carries the standing assumption of §2: $X$ is pure $n$-dimensional and $m$ is a weight. Orthogonality to the constants is always weighted by $m$ (or by $m_\tau$ in a link).

The adjoint $d^*$ is defined by its explicit formula; that it is the adjoint is Lemma 3.6. The eigenvalue condition $\mu_\tau\le\lambda$ is stated in Rayleigh form: $\langle (M')^+_{\tau,0}g,g\rangle\le\lambda\|g\|^2$ for every $g$ on the vertices of $X_\tau$ that is $m_\tau$-orthogonal to the constants. It is equivalent to the eigenvalue form even for disconnected links. A Rayleigh bound over all $g$, constants included, would be unsatisfiable for $\lambda<1$ and would make the goal vacuous; it is ruled out. The predicate quantifies over every face of dimension $-1$ to $n-2$, including $\emptyset$.

Corrections, all disclosed in the items:

• Lemma 4.3 is stated with a bound $\mu\ge\max(\mu_k,0)$. The printed version with $\mu_k<0$ fails already for the complete graph on three vertices.
• Corollary 5.3 accordingly takes $\mu_i\ge0$ and $\lambda\ge0$. Its two formal statements retain the page's assumption that every link of dimension at least one is connected, including $X$ itself.
• The proof of Theorem 5.4 ends with $(k+1)\lambda$; the statement's $\frac{k+1}{2}\lambda$ is formalized.

Welcome contributions: proofs of any milestone. Reusable lemmas on finite weighted inner products, on double counting over faces of a Finset (Finset V), and on links are useful beyond this mission; the companion mission on two-sided expanders uses the same objects.

Selected references

• T. Kaufman, I. Oppenheim, High Order Random Walks: Beyond Spectral Gap, arXiv:1707.02799v3, 2021. https://arxiv.org/abs/1707.02799
• N. Anari, K. Liu, S. Oveis Gharan, C. Vinzant, Log-concave polynomials II: High-dimensional walks and an FPRAS for counting bases of a matroid, STOC 2019. https://arxiv.org/abs/1811.01816
• H. Garland, p-adic curvature and the cohomology of discrete subgroups of p-adic groups, Ann. of Math. 97:375–423, 1973. https://doi.org/10.2307/1970781
• T. Kaufman, D. Mass, High dimensional random walks and colorful expansion, ITCS 2017. https://arxiv.org/abs/1604.02947
• I. Oppenheim, Local spectral expansion approach to high dimensional expanders Part I: Descent of spectral gaps, Discrete Comput. Geom. 59(2):293–330, 2018. https://arxiv.org/abs/1709.04431

Multiscale reaction networks and the balance condition

Stochastic models of chemical reaction networks in cell biology routinely combine species present in a handful of copies with species present in thousands, and rate constants that differ by orders of magnitude. Simulating such a system exactly is expensive, and model reduction replaces it with a lower-dimensional limit. A systematic approach, developed by Ball, Kurtz, Popovic and Rempala (2006) and by Kang and Kurtz (arXiv:1011.1672), normalizes species numbers and rate constants by powers of a large parameter $N$ and derives limits as $N\to\infty$ on several time-scales.

For such limits to exist, the normalized species numbers must stay of order one. For a single species this is the species balance condition: either the fastest reaction producing it is as fast as the fastest reaction consuming it, or the time-scale considered is short enough that the imbalance does not show. Kang and Kurtz observed (arXiv:1011.1672v1, §3.2, p. 9) that this is not enough: a collection of species can be produced collectively at a different order of magnitude from the rate at which it is consumed, even when every member is balanced. They therefore impose a balance condition on every nonnegative linear combination of species, which is infinitely many conditions. Section 3.4 of their paper proves combinatorial lemmas that reduce the work of checking them. This mission formalizes the lemmas on positive combinations of two weight vectors.

Setting

A reaction network has $s_0$ species $S_1,\dots,S_{s_0}$ and $r_0$ reactions. Reaction $k$ consumes $\nu_{ik}\in\mathbb N$ molecules of $S_i$ and produces $\nu'_{ik}\in\mathbb N$; its net change is the vector $\zeta_k=\nu'_k-\nu_k$. Each species carries a scaling exponent $\alpha_i\ge0$ and each reaction an exponent $\beta_k\in\mathbb R$; put

$$\rho_k=\beta_k+\nu_k\cdot\alpha=\beta_k+\sum_i\nu_{ik}\alpha_i,$$

the order of magnitude (as a power of $N$) of the rate of reaction $k$.

A weight vector $\theta\in[0,\infty)^{s_0}$ describes the linear combination $\theta\cdot X=\sum_i\theta_iX_i$. Its sign sets (Definition 3.1) are

$$\Gamma^+_\theta=\{k:\theta\cdot\zeta_k>0\},\qquad\Gamma^-_\theta=\{k:\theta\cdot\zeta_k<0\},$$

the reactions that increase and decrease $\theta\cdot X$. Maxima $\max_{k\in S}\rho_k$ are taken in $\mathbb R\cup\{-\infty\}$, with $\max_{k\in\emptyset}\rho_k=-\infty$, and $a\vee b$ is the maximum.

Fix a time-scale exponent $\gamma\in\mathbb R$. Condition 3.2 holds for $\theta$ if either the balance equation

$$\max_{k\in\Gamma^-_\theta}\rho_k=\max_{k\in\Gamma^+_\theta}\rho_k\tag{3.7}$$

or the time-scale constraint

$$\gamma\le\gamma_\theta\equiv\max_{i:\theta_i>0}\alpha_i-\max_{k\in\Gamma^+_\theta\cup\Gamma^-_\theta}\rho_k\tag{3.8}$$

holds, with $\gamma_\theta=+\infty$ when $\Gamma^+_\theta\cup\Gamma^-_\theta=\emptyset$.

Formalization targets

Goal: Lemma 3.8 (p. 18)

Let $\theta^1,\theta^2\in[0,\infty)^{s_0}$, $c_1,c_2>0$, and suppose

$$\Gamma^+_{\theta^1}\cap\Gamma^-_{\theta^2}=\emptyset\quad\text{or}\quad\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset.$$

Then (i) if Condition 3.2 holds for $\theta^1$ and $\theta^2$, it holds for $c_1\theta^1+c_2\theta^2$; and (ii) if (3.7) holds for $\theta^1$ and $\theta^2$, it holds for $c_1\theta^1+c_2\theta^2$.

Milestones, in the order the paper uses them

1. (3.16)–(3.17) (p. 15): $\Gamma^\pm_{c_1\theta^1+c_2\theta^2}\subseteq\Gamma^\pm_{\theta^1}\cup\Gamma^\pm_{\theta^2}$, hence

$$\max_{k\in\Gamma^\pm_{c_1\theta^1+c_2\theta^2}}\rho_k\le\max_{k\in\Gamma^\pm_{\theta^1}}\rho_k\vee\max_{k\in\Gamma^\pm_{\theta^2}}\rho_k.$$

2. Lemma 3.5 (p. 17): (3.8) for $\theta^1,\dots,\theta^m$ implies (3.8) for $\sum_jc_j\theta^j$, $c_j>0$.
3. Lemma 3.6 (p. 17): if $\max_{\Gamma^-_{\theta^1}}\rho=\max_{\Gamma^+_{\theta^1}}\rho>\max_{\Gamma^+_{\theta^2}\cup\Gamma^-_{\theta^2}}\rho$, then (3.7) holds for $c_1\theta^1+c_2\theta^2$.
4. Lemma 3.7 (p. 18): (3.7) for $\theta^1$ and (3.8) for $\theta^2$ give Condition 3.2 for $c_1\theta^1+c_2\theta^2$.
5. (3.35)–(3.36) (p. 19): if $\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset$, then

$$\max_{\Gamma^-_{\theta^1}}\rho\le\max_{\Gamma^-_{c_1\theta^1+c_2\theta^2}}\rho\le\max_{\Gamma^-_{\theta^1}}\rho\vee\max_{\Gamma^-_{\theta^2}}\rho,\quad\max_{\Gamma^+_{\theta^2}}\rho\le\max_{\Gamma^+_{c_1\theta^1+c_2\theta^2}}\rho\le\max_{\Gamma^+_{\theta^1}}\rho\vee\max_{\Gamma^+_{\theta^2}}\rho.$$

Companion results

• Remark 3.9 (p. 18): if no reaction that consumes a species in the support of $\theta^1$ produces a species in the support of $\theta^2$, then $\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2}=\emptyset$.
• Lemma 3.10 (p. 19): if (3.7) holds for $\theta^1$, $\theta^2$ and for $\theta^1-\frac{\theta^1\cdot\zeta_k}{\theta^2\cdot\zeta_k}\theta^2$ for every $k\in(\Gamma^+_{\theta^1}\cap\Gamma^-_{\theta^2})\cup(\Gamma^-_{\theta^1}\cap\Gamma^+_{\theta^2})$, then (3.7) holds for $c_1\theta^1+c_2\theta^2$ for all $c_1,c_2>0$.

Significance

Condition 3.2 must hold for every $\theta\in[0,\infty)^{s_0}$ before the limit theorems of the paper's Sections 4–5 apply. Lemma 3.8, together with the decomposition over strongly connected components (Lemma 3.4, the subject of the first mission of this series), turns that infinite family into finitely many checks for many networks: once the condition is known for some generating vectors, it propagates to their positive combinations whenever the sign sets do not conflict. Remark 3.9 gives a condition on the stoichiometry alone under which they do not conflict, and Lemma 3.10 reduces checking balance along a ray of combinations to finitely many breakpoints.

The results are proved in the paper (arXiv:1011.1672v1, pp. 15–19; published in Ann. Appl. Probab. 23(2), 2013), but none is formalized anywhere to our knowledge. The printed proof of Lemma 3.10 is a sketch that treats only the first breakpoint of the ray $\theta^1+c\theta^2$; a machine-checked proof would settle it in full. The definitions of the sign sets, the balance equation and the time-scale constraint are reusable for the other missions of this series.

Difficulty

The proofs are elementary, and the work lies in the bookkeeping. Every statement mixes three conventions: maxima over sets that can be empty (value $-\infty$), a time-scale constant that can be $+\infty$, and strict versus weak sign conditions on $\theta\cdot\zeta_k$. Lemma 3.8 is a case analysis on which disjunct of Condition 3.2 holds for each of $\theta^1$ and $\theta^2$; the obvious idea of applying (3.16)–(3.17) alone fails in the case where both vectors are balanced at the same level ((3.34) in the paper), where only upper bounds are available. That case needs the disjointness hypothesis to get the matching lower bounds (3.35)–(3.36). Lemma 3.10 needs an argument along the whole ray $\theta^1+c\theta^2$, $c>0$: the sign pattern of $(\theta^1+c\theta^2)\cdot\zeta_k$ changes at finitely many values of $c$, and balance has to be tracked through each change, not only the first.

Formalization scope

Species are Fin s and reactions Fin r (0-based indices; $s_0,r_0$ are arbitrary naturals). ν k i is $\nu_{ik}$; $\zeta_{ik}$, $\rho_k$ and $\theta\cdot\zeta_k$ are real numbers, and $\rho$ is defined from $\nu,\alpha,\beta$ rather than taken as a free parameter. A combination $c_1\theta^1+c_2\theta^2$ is c₁ • θ₁ + c₂ • θ₂ on Fin s → ℝ. Maxima are Finset.sup into WithBot ℝ, so the maximum over the empty set is $\bot=-\infty$ and $\vee$ is ⊔. $\gamma_\theta$ is an EReal defined by cases: $+\infty$ if $\Gamma^+_\theta\cup\Gamma^-_\theta=\emptyset$, otherwise the difference of the two maxima computed in $\mathbb R$ (or $-\infty$ if no $\theta_i$ is positive). Every statement carries the paper's standing assumptions $\alpha\ge0$, $\theta^1,\theta^2\ge0$ and $c_1,c_2>0$.

These choices rule out the trivializing encodings: a real-valued maximum with a default value of $0$ on the empty set would make the balance equation hold spuriously; a subtraction in EReal would turn $-\infty-(-\infty)$ into $-\infty$; and dropping $\theta\ge0$ or $c_1,c_2>0$ would change which reactions lie in the sign sets of the combination. In Lemma 3.8 the disjointness of the sign sets is a disjunction, as printed, and the second paragraph's "Condition 3.7" is read as the balance equation (3.7).

The development needs only finite sets, finite sums and order on $\mathbb R\cup\{\pm\infty\}$; no probability theory is involved. Lemmas about Finset.sup into WithBot ℝ over unions and subsets are reusable. Proofs of the milestones, of the goal, and of Lemma 3.10 are all welcome.

Selected references

• H.-W. Kang and T. G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010; Ann. Appl. Probab. 23(2), 2013. https://arxiv.org/abs/1011.1672, https://doi.org/10.1214/12-AAP841
• K. Ball, T. G. Kurtz, L. Popovic and G. Rempala, Asymptotic analysis of multiscale approximations to reaction networks, Ann. Appl. Probab. 16(4):1925–1961, 2006. https://doi.org/10.1214/105051606000000420
• Y. Cao, D. T. Gillespie and L. R. Petzold, The slow-scale stochastic simulation algorithm, J. Chem. Phys. 122(1):014116, 2005. https://doi.org/10.1063/1.1824902

Motivation

Chemical reaction networks can contain reactions whose rates differ by powers of a large scaling parameter. A species may then change on one time scale while other combinations of species remain nearly fixed until a later one. This matters when replacing a detailed network by a smaller model: the quantities retained at the first scale need not be the quantities that evolve at the next. Kang and Kurtz formulate this separation using the reaction exponents and the changes made by each reaction, before analyzing the stochastic process limits in their paper. This mission concerns the algebraic separation of the first two natural time scales in Lemma 4.4, rather than a convergence theorem for the stochastic processes.

Setting

A reaction network has a finite set of species and a finite set of indexed reactions. For reaction $k$, the nonnegative integer $\nu_{ik}$ is the number of molecules of species $i$ consumed, and $\nu'_{ik}$ is the number produced. Its net change is $\zeta_{ik}=\nu'_{ik}-\nu_{ik}$. The two reaction vectors may coincide; allowing such a reaction does not make it change any species. The paper introduces a nonnegative abundance exponent $\alpha_i$ for each species and a real rate exponent $\beta_k$ for each reaction. The exponent relevant to a reaction under that abundance scaling is $\rho_k=\beta_k+\sum_i\nu_{ik}\alpha_i$ §2 and §3.2.

A nonnegative vector $\theta$ assigns weights to the species. The weighted quantity changes by $\theta\cdot\zeta_k$ when reaction $k$ occurs. Define $\Gamma^+_\theta$ and $\Gamma^-_\theta$ as the reactions for which this dot product is respectively positive and negative. Let $\alpha_\theta$ be the greatest $\alpha_i$ among indices with $\theta_i>0$. The natural time scale of this combination is

$$\gamma_\theta=\alpha_\theta-\max_{k\in\Gamma^+_\theta\cup\Gamma^-_\theta}\rho_k.$$

An empty maximum is $-\infty$, so a combination unaffected by every reaction has $\gamma_\theta=+\infty$. In particular $\gamma_0=+\infty$; the unused value of $\alpha_0$ has no effect. A coordinate vector gives a single species' scale $\gamma_i$. The first time scale is $r_1=\min_i\gamma_i$ (3.5), Definition 3.1, and (4.1).

At scale $r_1$, define $\Gamma_i^{r_1}=\{k:r_1+\rho_k=\alpha_i\}$. It contains every reaction meeting that exponent equation, including one that leaves species $i$ unchanged. Let $\mathbb S_1$ consist of the coordinate vectors $e_i$ for which $\Gamma_i^{r_1}$ is nonempty, and let $\Pi_1$ be the coordinate projection onto their span. The nonnegative combinations whose projection is unchanged by each such reaction form

$$\mathbb K_2=\left\{\theta\geq0:\theta\cdot\Pi_1\zeta_k=0\quad \text{for every }k\in\bigcup_i\Gamma_i^{r_1}\right\}.$$

The second time scale is $r_2=\inf_{\theta\in\mathbb K_2}\gamma_\theta$. This is the paper's minimum over $\mathbb K_2$: despite the infinite set of eligible vectors, every finite value of $\gamma_\theta$ is a difference of one of finitely many $\alpha_i$ and one of finitely many $\rho_k$ §4, p. 21.

Formalization targets

The first milestone compares each weighted combination with the species in its positive support and identifies $r_1$ among all nonnegative combinations:

$$\gamma_\theta\geq\min_{i:\theta_i>0}\gamma_i, \qquad r_1=\inf_{\eta\geq0}\gamma_\eta.$$

The second milestone is the first sentence of Lemma 4.4. For $\theta\in\mathbb K_2$ and $l\in\Gamma_i^{r_1}$, a nonzero $\theta\cdot\zeta_l$ implies $\alpha_\theta>\alpha_i$. The goal is the lemma's strict separation:

$$r_2>r_1.$$

These statements and their source order are on p. 21 of the preprint. The goal allows $r_2=+\infty$, which represents the absence of a later changing combination in $\mathbb K_2$.

Significance

The strict inequality says that the quantities eligible for the second scale cannot move at the first scale. It makes the two-scale terminology precise for this exponent model and separates an algebraic fact about reaction vectors from the later analysis of stochastic limits. A reduced process on the second scale requires additional stability and convergence conditions; Lemma 4.4 alone supplies neither. The paper explicitly discusses that limitation immediately after its proof on p. 22.

This mission packages the reaction-exponent definitions and the scale-separation statements as Lean declarations. Their proof obligations remain open in the proposal. Reusable parts include the finite reaction indexing, real-valued net-change vectors, the explicit convention for empty maxima, and the extended-real scale definitions. A complete development may also establish supporting facts about the finite range of $\gamma_\theta$ and the coordinate projection; such facts are useful beyond this lemma. The paper's stochastic limit theorems are outside this mission's scope.

Difficulty

Checking separately that every $\theta\in\mathbb K_2$ has $\gamma_\theta>r_1$ does not establish $r_2>r_1$: an infimum of strictly larger values can still equal $r_1$. The statement needs the finite-range property of the scale function, together with the interaction between the fast-reaction equation defining $\Gamma_i^{r_1}$ and the projected orthogonality condition defining $\mathbb K_2$. Empty reaction sets and zero weighted combinations also require explicit extended-real values. Replacing their scales with a default real number would change the claim Lemma 4.4, pp. 21–22.

Formalization scope

Species and reactions are Fin s and Fin r; their indices begin at zero, while the paper numbers them from one. The stoichiometric arrays have natural-number entries, $\zeta$ and $\rho$ are real-valued, and theorems carry $\alpha_i\geq0$. The sets of changing reactions and the positive support of $\theta$ are finite sets. Empty maxima use a bottom-extended real, while $\gamma_i$, $\gamma_\theta$, $r_1$, and $r_2$ live in extended reals. Finite scale differences are calculated in the reals before conversion. The formulas define $\rho$ from $\nu,\alpha,\beta$ and construct $\mathbb K_2$ from $r_1$; neither is a free input. No extra positivity condition is imposed on $\beta$.

The coordinate projection $\Pi_1$ retains the indices belonging to $\mathbb S_1$. The infimum for $r_2$ ranges over all of $\mathbb K_2$, including the zero vector and combinations unchanged by every reaction. The goal assumes that some reaction changes a species. Without this necessary nondegeneracy condition, $r_1=r_2=+\infty$ and the strict conclusion is false. It adds no condition on the initial stochastic state: the assumption at the start of §4 belongs to its process-limit statements. The paper develops at-most-binary mass-action rates in §2, but Lemma 4.4 uses only the indexed reaction vectors and their exponents; the Lean declarations expose exactly those algebraic data.

Selected references

• H.-W. Kang and T. G. Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, 2010; published in Annals of Applied Probability 23(2), 2013. Preprint, DOI.