Lemma 4.4, p. 21 — the second time scale exceeds the first

Proved

KangKurtz.SecondScale.lemma_4_4

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

multiscalep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1reaction-networkstime-scales

For a finite reaction network, let $r_1=\min_i\gamma_i$ be the first natural time scale. Let $\mathbb K_2$ consist of the nonnegative weighted combinations unchanged by the projected first-scale reactions, and set $r_2=\inf_{\theta\in\mathbb K_2}\gamma_\theta$ . If at least one reaction changes at least one species, then

r_2>r_1.

This separates the first and second natural time scales defined in Section 4.

Formalization Note The requirement that some $\zeta_{ik}\ne0$ makes $r_1$ finite. It is a necessary explicit addition: if every reaction has zero net change, both time scales are $+\infty$ and the strict inequality is false. The infimum is over all of $\mathbb K_2$ , including combinations unchanged by every reaction.

Preamble

import Mathlib
import Definitions.Def_KangKurtz_SecondScale_Setting

Formal statement

namespace KangKurtz.SecondScale

theorem lemma_4_4 {s r : ℕ} (ν ν' : Fin r → Fin s → ℕ)
    (α : Fin s → ℝ) (hα : ∀ i, 0 ≤ α i) (β : Fin r → ℝ)
    (hζ : ∃ k i, ν' k i ≠ ν k i) :
    r1 ν ν' α β < r2 ν ν' α β := by sorry

end KangKurtz.SecondScale

Source

Kang and Kurtz, Separation of time-scales and model reduction for stochastic reaction networks, arXiv:1011.1672v1, p. 21, Lemma 4.4, second part

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph