CRNs are population protocols (CRN-1)

The population protocol of a network N runs on n agents, each holding a species. In one interaction it draws a uniformly random ordered pair (u, v) of distinct agents and, independently, a uniformly random reaction r of N. The pair reacts if the species of u and v are the reactants of r, and then r fires; otherwise nothing changes. Drawing the reaction uniformly is what a common rate constant means when several reactions share their reactants (as X + Y → X + B and X + Y → Y + B in approximate majority). We observe the protocol on count vectors, which do not depend on which agent receives which product.

Key identity (pair_prob_of_ne, pair_prob_of_eq): the pair has species {A, B} with probability #A·#B / C(n, 2), or C(#A, 2) / C(n, 2) if A = B. This is the mass-action propensity divided by the common factor k·C(n, 2) (pair_prob_eq_propensity). Hence the protocol reacts with probability a₀(x) / (k·|N|·C(n, 2)) (reactProb_eq), each interaction is a jump of the mass-action chain with that probability and a no-op otherwise (ppStep_expect), and conditioned on the pair reacting the protocol is exactly the jump chain (condStep_eq_jumpKernel, and jumpKernel_eq_ppKernel as kernels on count vectors).

@[reducible, inline]

abbrev Crn.AgentPair (n : ℕ) : Type

An ordered pair (u, v) of distinct agents among n (initiator and responder).

Equations

• Crn.AgentPair n = { p : Fin n × Fin n // p.1 ≠ p.2 }

theorem Crn.agentPair_nonempty {n : ℕ} (hn : 2 ≤ n) : Nonempty (AgentPair n)

With at least two agents there is a pair of distinct agents.

noncomputable def Crn.pairDist {n : ℕ} (hn : 2 ≤ n) : Dynamics.Distribution (AgentPair n)

The scheduler of the population protocol: a uniformly random ordered pair of distinct agents.

Equations

• Crn.pairDist hn = Dynamics.Distribution.uniform (Crn.AgentPair n)

def Crn.counts {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (c : Fin n → S) : Counts S n

The count vector of a configuration c (agent v holds species c v).

Equations

• Crn.counts c = ⟨fun (a : S) => {v : Fin n | c v = a}.card, ⋯⟩

noncomputable def Crn.sampleDist {S : Type u_1} {n : ℕ} (N : Network S) (hn : 2 ≤ n) : Dynamics.Distribution (AgentPair n × ↥N.reactions)

One draw of the population protocol of N: a uniformly random ordered pair of distinct agents and, independently, a uniformly random reaction of N.

Equations

• Crn.sampleDist N hn = Dynamics.Distribution.uniform (Crn.AgentPair n × ↥N.reactions)

def Crn.Reacts {S : Type u_1} {n : ℕ} (N : Network S) (c : Fin n → S) (ω : AgentPair n × ↥N.reactions) : Prop

In configuration c, the drawn pair reacts by the drawn reaction: the species of the two agents are the reactants of the reaction.

Equations

• Crn.Reacts N c ω = (s(c (↑ω.1).1, c (↑ω.1).2) = (↑ω.2).reactants)

@[implicit_reducible]

instance Crn.instDecidablePredReacts {S : Type u_1} [DecidableEq S] {n : ℕ} (N : Network S) (c : Fin n → S) : DecidablePred (Reacts N c)

Equations

• Crn.instDecidablePredReacts N c x✝ = id inferInstance

def Crn.outcome {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) (c : Fin n → S) (ω : AgentPair n × ↥N.reactions) : Counts S n

The count vector after the interaction ω from configuration c: the drawn reaction fires if the drawn pair reacts by it.

Equations

• Crn.outcome N c ω = if Crn.Reacts N c ω then (Crn.counts c).react ↑ω.2 else Crn.counts c

noncomputable def Crn.ppStep {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) (hn : 2 ≤ n) (c : Fin n → S) : Dynamics.Distribution (Counts S n)

One interaction of the population protocol of N from configuration c, observed on count vectors.

Equations

• Crn.ppStep N hn c = (Crn.sampleDist N hn).map (Crn.outcome N c)

noncomputable def Crn.condStep {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) (hn : 2 ≤ n) (c : Fin n → S) : Dynamics.Distribution (Counts S n)

One interaction of the population protocol of N from configuration c, conditioned on the drawn pair reacting, observed on count vectors. If no pair can react, nothing changes.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Crn.ppKernel {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) (hn : 2 ≤ n) : Dynamics.Kernel (Counts S n)

The population protocol of N conditioned on reacting pairs, as a kernel on count vectors: from x, one conditioned interaction from some configuration with counts x (one exists; condStep_eq_jumpKernel shows that the choice does not matter).

Equations

• Crn.ppKernel N hn x = if h : ∃ (c : Fin n → S), Crn.counts c = x then Crn.condStep N hn h.choose else Dynamics.Distribution.point x

Helper lemmas

theorem Crn.counts_val {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (c : Fin n → S) (a : S) : ↑(counts c) a = {v : Fin n | c v = a}.card

The count of species a in a configuration.

theorem Crn.exists_counts_eq {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (x : Counts S n) : ∃ (c : Fin n → S), counts c = x

Every count vector is the count vector of some configuration.

theorem Crn.pairDist_prob {n : ℕ} (hn : 2 ≤ n) (E : AgentPair n → Prop) [DecidablePred E] : (pairDist hn).prob E = ↑(Finset.filter E Finset.univ).card / ↑(n * (n - 1))

The probability of an event under the scheduler: a counting ratio over the n·(n - 1) ordered pairs of distinct agents.

theorem Crn.cast_mul_pred (m : ℕ) : ↑(m * (m - 1)) = 2 * ↑(m.choose 2)

m·(m - 1) = 2·C(m, 2), cast to ℝ.

theorem Crn.choose_two_pos {n : ℕ} (hn : 2 ≤ n) : 0 < ↑(n.choose 2)

C(n, 2) > 0 for n ≥ 2.

theorem Crn.sampleDist_expect {S : Type u_1} {n : ℕ} (N : Network S) (hn : 2 ≤ n) (F : AgentPair n × ↥N.reactions → ℝ) : (sampleDist N hn).expect F = (∑ r : ↥N.reactions, (pairDist hn).expect fun (p : AgentPair n) => F (p, r)) / ↑N.reactions.card

Expectation under one draw of the protocol: the pair is averaged first, then the reaction.

theorem Crn.pair_prob_of_ne {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (hn : 2 ≤ n) (c : Fin n → S) {A B : S} (hAB : A ≠ B) : ((pairDist hn).prob fun (p : AgentPair n) => s(c (↑p).1, c (↑p).2) = s(A, B)) = ↑(↑(counts c) A) * ↑(↑(counts c) B) / ↑(n.choose 2)

Key identity (roadmap CRN-1), A ≠ B: a uniformly random ordered pair of distinct agents has species {A, B} with probability #A·#B / C(n, 2).

theorem Crn.pair_prob_of_eq {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (hn : 2 ≤ n) (c : Fin n → S) (A : S) : ((pairDist hn).prob fun (p : AgentPair n) => s(c (↑p).1, c (↑p).2) = s(A, A)) = ↑((↑(counts c) A).choose 2) / ↑(n.choose 2)

Key identity (roadmap CRN-1), A = B: a uniformly random ordered pair of distinct agents has species {A, A} with probability C(#A, 2) / C(n, 2).

theorem Crn.pair_prob_eq_propensity {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} {k : ℝ} (hk : 0 < k) (hn : 2 ≤ n) (c : Fin n → S) (r : Reaction S) : ((pairDist hn).prob fun (p : AgentPair n) => s(c (↑p).1, c (↑p).2) = r.reactants) = Reaction.propensity k r (counts c) / (k * ↑(n.choose 2))

Key identity (roadmap CRN-1): the probability that a uniformly random ordered pair of distinct agents has the reactant species of r is the mass-action propensity of r divided by the common factor k·C(n, 2).

theorem Crn.sampleDist_expect_reacts {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) {k : ℝ} (hk : 0 < k) (hn : 2 ≤ n) (c : Fin n → S) (g : ↥N.reactions → ℝ) : ((sampleDist N hn).expect fun (ω : AgentPair n × ↥N.reactions) => if Reacts N c ω then g ω.2 else 0) = (∑ r : ↥N.reactions, Reaction.propensity k (↑r) (counts c) * g r) / (k * ↑N.reactions.card * ↑(n.choose 2))

The core computation: the expectation of g(r) on the event that the drawn pair reacts by the drawn reaction r is ∑ᵣ aᵣ(x)·g(r) / (k·|N|·C(n, 2)).

theorem Crn.reactProb_eq {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) {k : ℝ} (hk : 0 < k) (hn : 2 ≤ n) (c : Fin n → S) : (sampleDist N hn).prob (Reacts N c) = N.totalPropensity k (counts c) / (k * ↑N.reactions.card * ↑(n.choose 2))

The drawn pair reacts with probability a₀(x) / (k·|N|·C(n, 2)), x the counts.

theorem Crn.ppStep_expect {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) {k : ℝ} (hk : 0 < k) (hn : 2 ≤ n) (c : Fin n → S) (f : Counts S n → ℝ) : (ppStep N hn c).expect f = (1 - (sampleDist N hn).prob (Reacts N c)) * f (counts c) + (sampleDist N hn).prob (Reacts N c) * (N.jumpKernel k hk n (counts c)).expect f

One interaction of the population protocol is a step of the mass-action jump chain with the probability that the drawn pair reacts, and a no-op otherwise.

theorem Crn.condStep_eq_jumpKernel {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) {k : ℝ} (hk : 0 < k) (hn : 2 ≤ n) (c : Fin n → S) : condStep N hn c = N.jumpKernel k hk n (counts c)

CRN-1, pointwise. From every configuration, one interaction of the population protocol conditioned on the pair reacting moves the count vector as one step of the jump chain of stochastic mass-action kinetics with a common rate constant.

theorem Crn.jumpKernel_eq_ppKernel {S : Type u_1} [Fintype S] [DecidableEq S] {n : ℕ} (N : Network S) {k : ℝ} (hk : 0 < k) (hn : 2 ≤ n) : N.jumpKernel k hk n = ppKernel N hn

CRN-1 (roadmap; Anderson–Kurtz 2011 for the jump chain). For a count-conserving bimolecular CRN with a common rate constant k, the jump chain of stochastic mass-action kinetics equals the population protocol picking a uniformly random ordered pair of distinct agents, conditioned on the pair reacting, as kernels on count vectors.