From population protocols to CRNs: helper lemmas (CRN-3)

• The reaction of a transition, p + q → δ₁(p, q) + δ₂(p, q) (Protocol.reactionOf), and the effect of an encounter on count vectors (counts_interact): the counts change exactly as by this reaction, which is applicable (consumed_le_counts); a transition that does not change the multiset of states does not change the counts (counts_interact_of_trivial).
• Conversely, a reaction with reactants s(p, q) applicable at the counts of a configuration comes from an encounter of two distinct agents in states p, q (exists_agentPair).
• Input tagging (Protocol.tagInputs): a protocol with one fresh state per input symbol, so that its input map is injective, which simulates the original protocol (tagInputs_stablyComputes).

Multiplicities

theorem Crn.count_mk {Q : Type u_2} [DecidableEq Q] (A B a : Q) : Multiset.count a s(A, B).toMultiset = (if A = a then 1 else 0) + if B = a then 1 else 0

Multiplicity of a in s(A, B), in the form [A = a] + [B = a].

The reaction of a transition

def Crn.Protocol.reactionOf {X : Type u_1} {Q : Type u_2} (P : Protocol X Q) (p q : Q) : Reaction Q

The reaction p + q → δ₁(p, q) + δ₂(p, q) of the transition δ(p, q).

Equations

• P.reactionOf p q = { reactants := s(p, q), products := s((P.δ (p, q)).1, (P.δ (p, q)).2) }

theorem Crn.counts_interact_add {X : Type u_1} {Q : Type u_2} {n : ℕ} [Fintype Q] [DecidableEq Q] (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) (a : Q) : ↑(counts (P.interact c e)) a + (P.reactionOf (c (↑e).1) (c (↑e).2)).consumed a = ↑(counts c) a + (P.reactionOf (c (↑e).1) (c (↑e).2)).produced a

The counts after an encounter, as an identity in ℕ: counts' + consumed = counts + produced.

theorem Crn.consumed_le_counts {X : Type u_1} {Q : Type u_2} {n : ℕ} [Fintype Q] [DecidableEq Q] (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) (a : Q) : (P.reactionOf (c (↑e).1) (c (↑e).2)).consumed a ≤ ↑(counts c) a

The reactants of the transition at an encounter are present.

theorem Crn.counts_interact {X : Type u_1} {Q : Type u_2} {n : ℕ} [Fintype Q] [DecidableEq Q] (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) : counts (P.interact c e) = (counts c).react (P.reactionOf (c (↑e).1) (c (↑e).2))

An encounter changes the counts as the reaction of its transition.

theorem Crn.counts_interact_of_trivial {X : Type u_1} {Q : Type u_2} {n : ℕ} [Fintype Q] [DecidableEq Q] (P : Protocol X Q) (c : Fin n → Q) (e : AgentPair n) (h : (P.reactionOf (c (↑e).1) (c (↑e).2)).reactants = (P.reactionOf (c (↑e).1) (c (↑e).2)).products) : counts (P.interact c e) = counts c

An encounter whose transition does not change the multiset of states does not change the counts.

theorem Crn.exists_agentPair {Q : Type u_2} {n : ℕ} [Fintype Q] [DecidableEq Q] (c : Fin n → Q) {p q : Q} (h : ∀ (a : Q), Multiset.count a s(p, q).toMultiset ≤ ↑(counts c) a) : ∃ (e : AgentPair n), c (↑e).1 = p ∧ c (↑e).2 = q

A reaction with reactants s(p, q) whose reactants are present comes from an encounter of two distinct agents in states p and q.

Input tagging

def Crn.Protocol.untag {X : Type u_1} {Q : Type u_2} (P : Protocol X Q) {k : ℕ} (eX : X ≃ Fin k) : Fin k ⊕ Q → Q

The state of the original protocol represented by a state of P.tagInputs eX.

Equations

• P.untag eX = Sum.elim (fun (j : Fin k) => P.input (eX.symm j)) id

def Crn.Protocol.tagInputs {X : Type u_1} {Q : Type u_2} (P : Protocol X Q) {k : ℕ} (eX : X ≃ Fin k) : Protocol X (Fin k ⊕ Q)

P with one fresh state inl j per input symbol: input i starts in inl (eX i), which behaves as P.input i; every encounter moves both agents to inr-states.

Equations

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

theorem Crn.untag_interact {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {k : ℕ} {eX : X ≃ Fin k} (c : Fin n → Fin k ⊕ Q) (e : AgentPair n) : P.untag eX ∘ (P.tagInputs eX).interact c e = P.interact (P.untag eX ∘ c) e

An encounter of the tagged protocol is an encounter of P on the represented states.

theorem Crn.reaches_untag {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {k : ℕ} {eX : X ≃ Fin k} {c d : Fin n → Fin k ⊕ Q} (h : (P.tagInputs eX).Reaches c d) : P.Reaches (P.untag eX ∘ c) (P.untag eX ∘ d)

Paths of the tagged protocol are paths of P on the represented states.

theorem Crn.lift_untag {X : Type u_1} {Q : Type u_2} {n : ℕ} {P : Protocol X Q} {k : ℕ} {eX : X ≃ Fin k} {c : Fin n → Fin k ⊕ Q} {d : Fin n → Q} (h : P.Reaches (P.untag eX ∘ c) d) : ∃ (c' : Fin n → Fin k ⊕ Q), (P.tagInputs eX).Reaches c c' ∧ P.untag eX ∘ c' = d

Paths of P from the represented configuration lift to the tagged protocol.

theorem Crn.tagInputs_stablyComputes {X : Type u_1} {Q : Type u_2} {P : Protocol X Q} {k : ℕ} {eX : X ≃ Fin k} [Fintype X] [DecidableEq X] {φ : (X → ℕ) → Bool} (h : P.StablyComputes φ) : (P.tagInputs eX).StablyComputes φ

Input tagging preserves stable computation.

theorem Crn.tagInputs_nontrivial {X : Type u_1} {Q : Type u_2} {P : Protocol X Q} {k : ℕ} {eX : X ≃ Fin k} (i : X) : ∃ (p : Fin k ⊕ Q) (q : Fin k ⊕ Q), s(p, q) ≠ s(((P.tagInputs eX).δ (p, q)).1, ((P.tagInputs eX).δ (p, q)).2)

The tagged protocol has a transition changing the multiset of states (from two copies of an input state to two inr-states).