Complex balancing and the deficiency-zero theorem

StructureChemical reaction network#✓fully proved

A chemical reaction network on the species S with reactions indexed by ρ: reaction r turns the source complex src r into the product complex prod r (stoichiometric coefficients).

structure ReactionNetwork (S ρ : Type*) where
  /-- The source (reactant) complex of each reaction. -/
  src : ρ → S → ℕ
  /-- The product complex of each reaction. -/
  prod : ρ → S → ℕ

Used by 31

Used byThe pseudo-Helmholtz function does not increase along solutions · Complexes of a chemical reaction network · Deficiency of a chemical reaction network · Horn–Feinberg: complex balancing for every choice of rate constants · Deficiency-zero theorem, weakly reversible case · Horn–Jackson: one equilibrium per compatibility class · Pseudo-Helmholtz function along positive mass-action solutions · Rate of change of the pseudo-Helmholtz function · Equality in the Horn–Jackson inequality · Horn–Jackson inequality · Complex-balanced concentrations · Horn–Jackson · Weakly reversible reaction network · Linkage graph of a reaction network · Mass-action vector field · Complex-balanced states are equilibria · Deficiency-zero theorem, non-weakly-reversible case · Number of linkage classes of a reaction network · Horn–Jackson: the positive equilibria · Mass-action reaction rate · Directed reaction relation on complexes · Stoichiometric subspace · Complex balance exchanges source and product sums · Generator of the mass-action chain on a finite state class · Stationary law of the stochastic mass-action chain on a finite class · State after one reaction firing · Restricted mass-action generator is a rate matrix · Global balance of the product-form Poisson weights · Anderson–Craciun–Kurtz on a finite class · Stochastic mass-action propensity · State before one reaction firing

DefinitionStoichiometric subspace#✓fully proved

The stoichiometric subspace: the span of the reaction vectors prod r - src r.

def stoichiometricSubspace : Submodule ℝ (S → ℝ) :=
  Submodule.span ℝ (Set.range fun r s => (N.prod r s : ℝ) - N.src r s)

Uses 1 · Used by 4

Statement usesChemical reaction network

Used byDeficiency of a chemical reaction network · Deficiency-zero theorem, weakly reversible case · Horn–Jackson: one equilibrium per compatibility class · Horn–Jackson: the positive equilibria

DefinitionMass-action vector field#✓fully proved

The mass-action vector field with rate constants k: x ↦ ∑_r k r (∏_s x_s ^ (src r s)) (prod r - src r).

noncomputable def massActionField [Fintype S] [Fintype ρ] (k : ρ → ℝ) (x : S → ℝ) :
    S → ℝ :=
  fun s => ∑ r, k r * (∏ s', x s' ^ N.src r s') * ((N.prod r s : ℝ) - N.src r s)

Uses 1 · Used by 11

Statement usesChemical reaction network

Used byThe pseudo-Helmholtz function does not increase along solutions · Deficiency-zero theorem, weakly reversible case · Horn–Jackson: one equilibrium per compatibility class · Pseudo-Helmholtz function along positive mass-action solutions · Rate of change of the pseudo-Helmholtz function · Equality in the Horn–Jackson inequality · Horn–Jackson inequality · Horn–Jackson · Complex-balanced states are equilibria · Deficiency-zero theorem, non-weakly-reversible case · Horn–Jackson: the positive equilibria

DefinitionMass-action reaction rate#✓fully proved

The mass-action rate k r * ∏_s c_s ^ (src r s) of reaction r at concentrations c.

noncomputable def rate [Fintype S] (k : ρ → ℝ) (c : S → ℝ) (r : ρ) : ℝ :=
  k r * ∏ s, c s ^ N.src r s

Uses 1 · Used by 8

Statement usesChemical reaction network

Used byEquality in the Horn–Jackson inequality · Horn–Jackson inequality · Complex-balanced concentrations · Horn–Jackson · Complex-balanced states are equilibria · Horn–Jackson: the positive equilibria · Complex balance exchanges source and product sums · Global balance of the product-form Poisson weights

DefinitionComplex-balanced concentrations#✓fully proved

Concentrations c are complex balanced for the rate constants k: at every complex z, the total rate of the reactions with source z equals the total rate of the reactions with product z. (Complexes that occur in no reaction give 0 = 0.)

def IsComplexBalanced [Fintype S] [Fintype ρ] (k : ρ → ℝ) (c : S → ℝ) : Prop :=
  ∀ z : S → ℕ, ∑ r ∈ univ.filter (fun r => N.src r = z), N.rate k c r =
    ∑ r ∈ univ.filter (fun r => N.prod r = z), N.rate k c r

Sources

• Horn & Jackson (1972); Feinberg (2019), ch. 15.

Uses 2 · Used by 12

Statement usesChemical reaction network · Mass-action reaction rate

Used byThe pseudo-Helmholtz function does not increase along solutions · Horn–Feinberg: complex balancing for every choice of rate constants · Horn–Jackson: one equilibrium per compatibility class · Equality in the Horn–Jackson inequality · Horn–Jackson inequality · Horn–Jackson · Complex-balanced states are equilibria · Horn–Jackson: the positive equilibria · Complex balance exchanges source and product sums · Stationary law of the stochastic mass-action chain on a finite class · Global balance of the product-form Poisson weights · Anderson–Craciun–Kurtz on a finite class

DefinitionPseudo-Helmholtz function#✓fully proved

The pseudo-Helmholtz function G(c) = ∑_s c_s (log c_s - log c*_s - 1) relative to the reference concentrations cstar (Horn & Jackson 1972). It is meaningful for positive c and cstar; elsewhere Real.log takes junk values.

noncomputable def pseudoHelmholtz [Fintype S] (cstar c : S → ℝ) : ℝ :=
  ∑ s, c s * (Real.log (c s) - Real.log (cstar s) - 1)

Used by 2

Used byThe pseudo-Helmholtz function does not increase along solutions · Pseudo-Helmholtz function along positive mass-action solutions

DefinitionRate of change of the pseudo-Helmholtz function#✓fully proved

The rate of change of the pseudo-Helmholtz function along the mass-action vector field, ∑_s (log c_s - log c*_s) f_s(c): the derivative of pseudoHelmholtz cstar at c > 0 applied to massActionField k c (hasDerivAt_pseudoHelmholtz).

noncomputable def helmholtzRate [Fintype S] [Fintype ρ] (k : ρ → ℝ) (cstar c : S → ℝ) : ℝ :=
  ∑ s, (Real.log (c s) - Real.log (cstar s)) * N.massActionField k c s

Uses 2 · Used by 6

Statement usesChemical reaction network · Mass-action vector field

Used byThe pseudo-Helmholtz function does not increase along solutions · Pseudo-Helmholtz function along positive mass-action solutions · Equality in the Horn–Jackson inequality · Horn–Jackson inequality · Horn–Jackson · Horn–Jackson: the positive equilibria

TheoremComplex balance exchanges source and product sums#✓fully proved

Complex balance at c rewrites the rate-weighted sum of any function of the products as the same sum over the sources (for all real c and k).

theorem sum_rate_mul_prod_eq [Fintype S] [Fintype ρ] {k : ρ → ℝ} {c : S → ℝ}
    (h : N.IsComplexBalanced k c) (g : (S → ℕ) → ℝ) :
    ∑ r, N.rate k c r * g (N.prod r) = ∑ r, N.rate k c r * g (N.src r)

Uses 3 · Used by 6

Statement usesChemical reaction network · Complex-balanced concentrations · Mass-action reaction rate

Used byEquality in the Horn–Jackson inequality · Horn–Jackson inequality · Horn–Jackson · Complex-balanced states are equilibria · Horn–Jackson: the positive equilibria · Global balance of the product-form Poisson weights

TheoremComplex-balanced states are equilibria#✓fully proved

A complex-balanced state is an equilibrium of the mass-action system (for all real c and k). Source: Horn & Jackson (1972).

theorem massActionField_eq_zero_of_isComplexBalanced [Fintype S] [Fintype ρ] {k : ρ → ℝ}
    {c : S → ℝ} (h : N.IsComplexBalanced k c) : N.massActionField k c = 0

Uses 5 · Used by 2

Statement usesChemical reaction network · Complex-balanced concentrations · Mass-action vector field

Proof usesMass-action reaction rate · Complex balance exchanges source and product sums

Used byEquality in the Horn–Jackson inequality · Horn–Jackson: the positive equilibria

TheoremHorn–Jackson inequality#✓fully proved

If c* is a positive complex-balanced equilibrium for positive rate constants, the pseudo-Helmholtz function does not increase along the mass-action vector field at any positive c. Source: Horn & Jackson (1972); Feinberg (2019), ch. 15.

theorem helmholtzRate_nonpos [Fintype S] [Fintype ρ] {k : ρ → ℝ} (hk : ∀ r, 0 < k r)
    {cstar : S → ℝ} (hcstar : ∀ s, 0 < cstar s) (hcb : N.IsComplexBalanced k cstar)
    {c : S → ℝ} (hc : ∀ s, 0 < c s) : N.helmholtzRate k cstar c ≤ 0

Uses 6 · Used by 1

Statement usesChemical reaction network · Complex-balanced concentrations · Rate of change of the pseudo-Helmholtz function

Proof usesMass-action vector field · Mass-action reaction rate · Complex balance exchanges source and product sums

Used byThe pseudo-Helmholtz function does not increase along solutions

TheoremEquality in the Horn–Jackson inequality#✓fully proved

Under the hypotheses of helmholtzRate_nonpos, the rate of change of the pseudo-Helmholtz function vanishes at a positive c exactly when c is an equilibrium. Source: Horn & Jackson (1972).

theorem helmholtzRate_eq_zero_iff [Fintype S] [Fintype ρ] {k : ρ → ℝ} (hk : ∀ r, 0 < k r)
    {cstar : S → ℝ} (hcstar : ∀ s, 0 < cstar s) (hcb : N.IsComplexBalanced k cstar)
    {c : S → ℝ} (hc : ∀ s, 0 < c s) :
    N.helmholtzRate k cstar c = 0 ↔ N.massActionField k c = 0

Uses 7 · Used by 2

Statement usesChemical reaction network · Complex-balanced concentrations · Rate of change of the pseudo-Helmholtz function · Mass-action vector field

Proof usesComplex-balanced states are equilibria · Mass-action reaction rate · Complex balance exchanges source and product sums

Used byHorn–Jackson · Horn–Jackson: the positive equilibria

TheoremHorn–Jackson#✓fully proved

If a mass-action system with positive rate constants has a positive complex-balanced equilibrium, then every positive equilibrium is complex balanced.

theorem isComplexBalanced_of_massActionField_eq_zero [Fintype S] [Fintype ρ] {k : ρ → ℝ}
    (hk : ∀ r, 0 < k r) {cstar : S → ℝ} (hcstar : ∀ s, 0 < cstar s)
    (hcb : N.IsComplexBalanced k cstar) {c : S → ℝ} (hc : ∀ s, 0 < c s)
    (hf : N.massActionField k c = 0) : N.IsComplexBalanced k c

Sources

• Horn & Jackson (1972); Feinberg (2019), ch. 15.

Uses 7

Statement usesChemical reaction network · Complex-balanced concentrations · Mass-action vector field

Proof usesRate of change of the pseudo-Helmholtz function · Equality in the Horn–Jackson inequality · Mass-action reaction rate · Complex balance exchanges source and product sums

TheoremHorn–Jackson: the positive equilibria#✓fully proved

If c* is a positive complex-balanced equilibrium for positive rate constants, the positive equilibria are exactly the positive c whose log c - log c* is orthogonal (for the dot product) to the stoichiometric subspace. Source: Horn & Jackson (1972); Feinberg (2019), ch. 15.

theorem positiveEquilibria_eq [Fintype S] [Fintype ρ] {k : ρ → ℝ} (hk : ∀ r, 0 < k r)
    {cstar : S → ℝ} (hcstar : ∀ s, 0 < cstar s) (hcb : N.IsComplexBalanced k cstar) :
    {c : S → ℝ | (∀ s, 0 < c s) ∧ N.massActionField k c = 0} =
      {c | (∀ s, 0 < c s) ∧ ∀ v ∈ N.stoichiometricSubspace,
        (fun s => Real.log (c s) - Real.log (cstar s)) ⬝ᵥ v = 0}

Uses 9 · Used by 1

Statement usesChemical reaction network · Complex-balanced concentrations · Mass-action vector field · Stoichiometric subspace

Proof usesRate of change of the pseudo-Helmholtz function · Equality in the Horn–Jackson inequality · Complex-balanced states are equilibria · Mass-action reaction rate · Complex balance exchanges source and product sums

Used byHorn–Jackson: one equilibrium per compatibility class

TheoremBirch's theorem, existence#✓fully proved

For any subspace W of S → ℝ and positive a, b there is a positive c with c - b ∈ W and log c - log a orthogonal to W (for the dot product). Source: Birch (1963); Horn & Jackson (1972).

theorem exists_pos_sub_mem_log_orthogonal [Fintype S] (W : Submodule ℝ (S → ℝ))
    {a b : S → ℝ} (ha : ∀ s, 0 < a s) (hb : ∀ s, 0 < b s) :
    ∃ c : S → ℝ, (∀ s, 0 < c s) ∧ c - b ∈ W ∧
      ∀ v ∈ W, (fun s => Real.log (c s) - Real.log (a s)) ⬝ᵥ v = 0

Used by 1

Used byHorn–Jackson: one equilibrium per compatibility class

TheoremBirch's theorem, uniqueness#✓fully proved

Two positive vectors whose difference lies in a subspace W and whose logarithms differ by a vector orthogonal to W are equal.

theorem eq_of_sub_mem_log_orthogonal [Fintype S] {W : Submodule ℝ (S → ℝ)} {c d : S → ℝ}
    (hc : ∀ s, 0 < c s) (hd : ∀ s, 0 < d s) (hW : c - d ∈ W)
    (horth : ∀ v ∈ W, (fun s => Real.log (c s) - Real.log (d s)) ⬝ᵥ v = 0) : c = d

Sources

• Birch (1963); Horn & Jackson (1972).

Used by 1

Used byHorn–Jackson: one equilibrium per compatibility class

TheoremHorn–Jackson: one equilibrium per compatibility class#✓fully proved

If a mass-action system with positive rate constants has a positive complex-balanced equilibrium, then each positive stoichiometric compatibility class (x₀ + 𝒮) ∩ ℝ_{>0}^S, x₀ > 0, contains exactly one positive equilibrium. Source: Horn & Jackson (1972); Feinberg (2019), ch. 15.

theorem existsUnique_equilibrium_of_isComplexBalanced [Fintype S] [Fintype ρ] {k : ρ → ℝ}
    (hk : ∀ r, 0 < k r) {cstar : S → ℝ} (hcstar : ∀ s, 0 < cstar s)
    (hcb : N.IsComplexBalanced k cstar) {x₀ : S → ℝ} (hx₀ : ∀ s, 0 < x₀ s) :
    ∃! x : S → ℝ, (∀ s, 0 < x s) ∧ x - x₀ ∈ N.stoichiometricSubspace ∧
      N.massActionField k x = 0

Uses 7

Statement usesChemical reaction network · Complex-balanced concentrations · Mass-action vector field · Stoichiometric subspace

Proof usesHorn–Jackson: the positive equilibria · Birch's theorem, uniqueness · Birch's theorem, existence

TheoremPseudo-Helmholtz function along positive mass-action solutions#✓fully proved

The pseudo-Helmholtz function has time derivative helmholtzRate along a solution of the mass-action system, at any time where the solution is positive.

theorem hasDerivAt_pseudoHelmholtz [Fintype S] [Fintype ρ] {k : ρ → ℝ} (cstar : S → ℝ)
    {x : ℝ → S → ℝ} {t : ℝ} (hx : HasDerivAt x (N.massActionField k (x t)) t)
    (hpos : ∀ s, 0 < x t s) :
    HasDerivAt (fun τ => pseudoHelmholtz cstar (x τ)) (N.helmholtzRate k cstar (x t)) t

Uses 4 · Used by 1

Statement usesChemical reaction network · Rate of change of the pseudo-Helmholtz function · Mass-action vector field · Pseudo-Helmholtz function

Used byThe pseudo-Helmholtz function does not increase along solutions

TheoremThe pseudo-Helmholtz function does not increase along solutions#✓fully proved

Along a solution of a mass-action system with positive rate constants and a positive complex-balanced equilibrium c*, positive and differentiable (two-sided) at every t ≥ 0, G(x t) is nonincreasing on [0, ∞).

theorem antitoneOn_pseudoHelmholtz [Fintype S] [Fintype ρ] {k : ρ → ℝ} (hk : ∀ r, 0 < k r)
    {cstar : S → ℝ} (hcstar : ∀ s, 0 < cstar s) (hcb : N.IsComplexBalanced k cstar)
    {x : ℝ → S → ℝ} (hx : ∀ t, 0 ≤ t → HasDerivAt x (N.massActionField k (x t)) t)
    (hpos : ∀ t, 0 ≤ t → ∀ s, 0 < x t s) :
    AntitoneOn (fun t => pseudoHelmholtz cstar (x t)) (Set.Ici 0)

Sources

• Horn & Jackson (1972).

Uses 7

Statement usesChemical reaction network · Complex-balanced concentrations · Mass-action vector field · Pseudo-Helmholtz function

Proof usesPseudo-Helmholtz function along positive mass-action solutions · Rate of change of the pseudo-Helmholtz function · Horn–Jackson inequality

DefinitionComplexes of a chemical reaction network#✓fully proved

The complexes of the network: the sources and products of its reactions.

def complexes : Set (S → ℕ) :=
  Set.range N.src ∪ Set.range N.prod

Uses 1 · Used by 6

Statement usesChemical reaction network

Used byDeficiency of a chemical reaction network · Horn–Feinberg: complex balancing for every choice of rate constants · Deficiency-zero theorem, weakly reversible case · Linkage graph of a reaction network · Deficiency-zero theorem, non-weakly-reversible case · Number of linkage classes of a reaction network

DefinitionDirected reaction relation on complexes#✓fully proved

The directed reaction relation on complexes: y ⟶ y' if some reaction has source y and product y'.

def Reacts (y y' : S → ℕ) : Prop :=
  ∃ r, N.src r = y ∧ N.prod r = y'

Uses 1 · Used by 2

Statement usesChemical reaction network

Used byWeakly reversible reaction network · Linkage graph of a reaction network

DefinitionLinkage graph of a reaction network#✓fully proved

The undirected reaction graph on the complexes: distinct complexes are adjacent when one reacts to the other.

def linkageGraph : SimpleGraph N.complexes :=
  SimpleGraph.fromRel fun c c' => N.Reacts c c'

Uses 3 · Used by 1

Statement usesChemical reaction network · Directed reaction relation on complexes · Complexes of a chemical reaction network

Used byNumber of linkage classes of a reaction network

DefinitionNumber of linkage classes of a reaction network#✓fully proved

The number of linkage classes: connected components of the undirected reaction graph.

noncomputable def numLinkageClasses [Finite N.complexes] : ℕ :=
  Nat.card N.linkageGraph.ConnectedComponent

Uses 3 · Used by 1

Statement usesChemical reaction network · Complexes of a chemical reaction network · Linkage graph of a reaction network

Used byDeficiency of a chemical reaction network

DefinitionDeficiency of a chemical reaction network#✓fully proved

The deficiency δ = n - ℓ - s (number of complexes, linkage classes, dimension of the stoichiometric subspace).

noncomputable def deficiency [Finite N.complexes] : ℤ :=
  (Nat.card N.complexes : ℤ) - N.numLinkageClasses -
    Module.finrank ℝ N.stoichiometricSubspace

Uses 4 · Used by 3

Statement usesChemical reaction network · Complexes of a chemical reaction network · Number of linkage classes of a reaction network · Stoichiometric subspace

Used byHorn–Feinberg: complex balancing for every choice of rate constants · Deficiency-zero theorem, weakly reversible case · Deficiency-zero theorem, non-weakly-reversible case

DefinitionWeakly reversible reaction network#✓fully proved

The network is weakly reversible: for every reaction y → y' there is a directed path of reactions from y' back to y.

def IsWeaklyReversible : Prop :=
  ∀ r, Relation.ReflTransGen N.Reacts (N.prod r) (N.src r)

Uses 2 · Used by 3

Statement usesChemical reaction network · Directed reaction relation on complexes

Used byHorn–Feinberg: complex balancing for every choice of rate constants · Deficiency-zero theorem, weakly reversible case · Deficiency-zero theorem, non-weakly-reversible case

TheoremHorn–Feinberg: complex balancing for every choice of rate constants#●ready to prove

A weakly reversible mass-action network of deficiency zero has, for any positive rate constants, a positive complex-balanced equilibrium. Together with existsUnique_equilibrium_of_isComplexBalanced this gives existsUnique_equilibrium.

theorem_wanted exists_pos_isComplexBalanced [Fintype S] [Fintype ρ] (hδ : N.deficiency = 0)
    (hwr : N.IsWeaklyReversible) {k : ρ → ℝ} (hk : ∀ r, 0 < k r) :
    ∃ c : S → ℝ, (∀ s, 0 < c s) ∧ N.IsComplexBalanced k c

Sources

• Horn (1972); Feinberg (1972); Feinberg (1987).

Uses 5

Statement usesChemical reaction network · Complex-balanced concentrations · Weakly reversible reaction network · Complexes of a chemical reaction network · Deficiency of a chemical reaction network

TheoremDeficiency-zero theorem, weakly reversible case#●ready to prove

A weakly reversible mass-action network of deficiency zero has, for any positive rate constants, exactly one equilibrium in each positive stoichiometric compatibility class.

theorem_wanted existsUnique_equilibrium [Fintype S] [Fintype ρ] (hδ : N.deficiency = 0)
    (hwr : N.IsWeaklyReversible) {k : ρ → ℝ} (hk : ∀ r, 0 < k r)
    {x₀ : S → ℝ} (hx₀ : ∀ s, 0 < x₀ s) :
    ∃! x : S → ℝ, (∀ s, 0 < x s) ∧ x - x₀ ∈ N.stoichiometricSubspace ∧
      N.massActionField k x = 0

Sources

• Horn (1972); Horn & Jackson (1972); Feinberg (1987).

Uses 6

Statement usesChemical reaction network · Weakly reversible reaction network · Complexes of a chemical reaction network · Deficiency of a chemical reaction network · Mass-action vector field · Stoichiometric subspace

TheoremDeficiency-zero theorem, non-weakly-reversible case#●ready to prove

A mass-action network of deficiency zero that is not weakly reversible has no positive equilibrium for any positive rate constants.

theorem_wanted not_exists_positive_equilibrium [Fintype S] [Fintype ρ]
    (hδ : N.deficiency = 0) (hwr : ¬ N.IsWeaklyReversible)
    {k : ρ → ℝ} (hk : ∀ r, 0 < k r) :
    ¬ ∃ x : S → ℝ, (∀ s, 0 < x s) ∧ N.massActionField k x = 0

Sources

• Feinberg (1987).

Uses 5

Statement usesChemical reaction network · Weakly reversible reaction network · Complexes of a chemical reaction network · Deficiency of a chemical reaction network · Mass-action vector field

24 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.