Documentation

Crn.ApproximateMajority

Worked instance: the approximate-majority CRN (CRN-1) #

The approximate-majority CRN of Angluin, Aspnes and Eisenstat (2008), which Cardelli and Csikász-Nagy (2012) identify with the cell-cycle switch, has species X, Y (the two opinions) and B (blank, or undecided) and four reactions with a common rate constant:

X + Y → X + B, X + Y → Y + B, B + X → X + X, B + Y → Y + Y.

From counts x with D = 2·#X·#Y + #B·(#X + #Y) > 0, its jump chain fires each of the two X + Y reactions with probability #X·#Y / D, B + X → X + X with probability #B·#X / D and B + Y → Y + Y with probability #B·#Y / D (network_jump_expect). By CRN-1 this is the sequential undecided-state dynamics on n agents, conditioned on the drawn pair reacting (network_jumpKernel_eq_ppKernel); a drawn pair reacts with probability D / (4·C(n, 2)) (network_reactProb_eq).

source
inductive Crn.ApproxMajority.Species :
Type

Species of the approximate-majority CRN: the two opinions X, Y and the blank B.

Instances For
    source
    @[implicit_reducible]
    instance Crn.ApproxMajority.instDecidableEqSpecies :
    DecidableEq Species
    Equations
    source
    @[implicit_reducible]
    instance Crn.ApproxMajority.instFintypeSpecies :
    Fintype Species
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def Crn.ApproxMajority.xyToXB :
    Reaction Species

    X + Y → X + B: an X turns a Y blank.

    Equations
    Instances For
      source
      def Crn.ApproxMajority.xyToYB :
      Reaction Species

      X + Y → Y + B: a Y turns an X blank.

      Equations
      Instances For
        source
        def Crn.ApproxMajority.bxToXX :
        Reaction Species

        B + X → X + X: an X recruits a blank.

        Equations
        Instances For
          source
          def Crn.ApproxMajority.byToYY :
          Reaction Species

          B + Y → Y + Y: a Y recruits a blank.

          Equations
          Instances For
            source
            def Crn.ApproxMajority.network :
            Network Species

            The approximate-majority CRN.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Crn.ApproxMajority.network_reactions :
              network.reactions = {xyToXB, xyToYB, bxToXX, byToYY}

              The four reactions of the approximate-majority CRN.

              source
              theorem Crn.ApproxMajority.network_sum (k : ℝ) {n : ℕ} (x : Counts Species n) (g : Counts Species n → ℝ) :
              ∑ r ∈ network.reactions, Reaction.propensity k r x * g (x.react r) = k * (↑(↑x Species.X) * ↑(↑x Species.Y) * g (x.react xyToXB) + ↑(↑x Species.X) * ↑(↑x Species.Y) * g (x.react xyToYB) + ↑(↑x Species.B) * ↑(↑x Species.X) * g (x.react bxToXX) + ↑(↑x Species.B) * ↑(↑x Species.Y) * g (x.react byToYY))

              Propensity-weighted sums over the four reactions.

              source
              theorem Crn.ApproxMajority.network_totalPropensity (k : ℝ) {n : ℕ} (x : Counts Species n) :
              network.totalPropensity k x = k * (2 * ↑(↑x Species.X) * ↑(↑x Species.Y) + ↑(↑x Species.B) * (↑(↑x Species.X) + ↑(↑x Species.Y)))

              The total propensity of the approximate-majority CRN: k·(2·#X·#Y + #B·(#X + #Y)).

              source
              theorem Crn.ApproxMajority.network_jump_expect {k : ℝ} (hk : 0 < k) {n : ℕ} (x : Counts Species n) (hD : 0 < 2 * ↑x Species.X * ↑x Species.Y + ↑x Species.B * (↑x Species.X + ↑x Species.Y)) (f : Counts Species n → ℝ) :
              (network.jumpKernel k hk n x).expect f = (↑(↑x Species.X) * ↑(↑x Species.Y) * f (x.react xyToXB) + ↑(↑x Species.X) * ↑(↑x Species.Y) * f (x.react xyToYB) + ↑(↑x Species.B) * ↑(↑x Species.X) * f (x.react bxToXX) + ↑(↑x Species.B) * ↑(↑x Species.Y) * f (x.react byToYY)) / (2 * ↑(↑x Species.X) * ↑(↑x Species.Y) + ↑(↑x Species.B) * (↑(↑x Species.X) + ↑(↑x Species.Y)))

              The jump chain of the approximate-majority CRN with rate constant k, from counts x with D = 2·#X·#Y + #B·(#X + #Y) > 0: each X + Y reaction fires with probability #X·#Y / D, B + X → X + X with probability #B·#X / D and B + Y → Y + Y with probability #B·#Y / D.

              source
              theorem Crn.ApproxMajority.network_reactProb_eq {n : ℕ} (hn : 2 ≤ n) (c : Fin n → Species) :
              (sampleDist network hn).prob (Reacts network c) = (2 * ↑(↑(counts c) Species.X) * ↑(↑(counts c) Species.Y) + ↑(↑(counts c) Species.B) * (↑(↑(counts c) Species.X) + ↑(↑(counts c) Species.Y))) / (4 * ↑(n.choose 2))

              In the population protocol of the approximate-majority CRN, the drawn pair reacts with probability (2·#X·#Y + #B·(#X + #Y)) / (4·C(n, 2)).

              source
              theorem Crn.ApproxMajority.network_jumpKernel_eq_ppKernel {k : ℝ} (hk : 0 < k) {n : ℕ} (hn : 2 ≤ n) :
              network.jumpKernel k hk n = ppKernel network hn

              CRN-1 for approximate majority: its jump chain is the population protocol conditioned on the drawn pair reacting.