text:
\section{Typesetting instructions -- Summary}
\label{sec:typesetting-summary}

LIPIcs is a series of open access high-quality conference proceedings across all fields in informatics established in cooperation with Schloss Dagstuhl.
In order to do justice to the high scientific quality of the conferences that publish their proceedings in the LIPIcs series, which is ensured by the thorough review process of the respective events, we believe that LIPIcs proceedings must have an attractive and consistent layout matching the standard of the series.
Moreover, the quality of the metadata, the typesetting and the layout must also meet the requirements of other external parties such as indexing service, DOI registry, funding agencies, among others. The guidelines contained in this document serve as the baseline for the authors, editors, and the publisher to create documents that meet as many different requirements as possible.

Please comply with the following instructions when preparing your article for a LIPIcs proceedings volume.
\paragraph*{Minimum requirements}

\begin{itemize}
\item Use pdflatex and an up-to-date \LaTeX{} system.
\item Use further \LaTeX{} packages and custom made macros carefully and only if required.
\item Use the provided sectioning macros: \verb+\section+, \verb+\subsection+, \verb+\subsubsection+, \linebreak \verb+\paragraph+, \verb+\paragraph*+, and \verb+\subparagraph*+.
\item Provide suitable graphics of at least 300dpi (preferably in PDF format).
\item Use BibTeX and keep the standard style (\verb+plainurl+) for the bibliography.
\item Please try to keep the warnings log as small as possible. Avoid overfull \verb+\hboxes+ and any kind of warnings/errors with the referenced BibTeX entries.
\item Use a spellchecker to correct typos.
\end{itemize}

\paragraph*{Mandatory metadata macros}
Please set the values of the metadata macros carefully since the information parsed from these macros will be passed to publication servers, catalogues and search engines.
Avoid placing macros inside the metadata macros. The following metadata macros/environments are mandatory:
\begin{itemize}
\item \verb+\title+ and, in case of long titles, \verb+\titlerunning+.
\item \verb+\author+, one for each author, even if two or more authors have the same affiliation.
\item \verb+\authorrunning+ and \verb+\Copyright+ (concatenated author names)\\
The \verb+\author+ macros and the \verb+\Copyright+ macro should contain full author names (especially with regard to the first name), while \verb+\authorrunning+ should contain abbreviated first names.
\item \verb+\ccsdesc+ (ACM classification, see \url{https://www.acm.org/publications/class-2012}).
\item \verb+\keywords+ (a comma-separated list of keywords).
\item \verb+\relatedversion+ (if there is a related version, typically the ``full version''); please make sure to provide a persistent URL, e.\,g., at arXiv.
\item \verb+\begin{abstract}...\end{abstract}+ .
\end{itemize}

\paragraph*{Please do not \ldots}
Generally speaking, please do not override the \texttt{lipics-v2019}-style defaults. To be more specific, a short checklist also used by Dagstuhl Publishing during the final typesetting is given below.
In case of \textbf{non-compliance} with these rules Dagstuhl Publishing will remove the corresponding parts of \LaTeX{} code and \textbf{replace it with the \texttt{lipics-v2019} defaults}. In serious cases, we may reject the LaTeX-source and expect the corresponding author to revise the relevant parts.
\begin{itemize}
\item Do not use a different main font. (For example, the \texttt{times} package is forbidden.)
\item Do not alter the spacing of the \texttt{lipics-v2019.cls} style file.
\item Do not use \verb+enumitem+ and \verb+paralist+. (The \texttt{enumerate} package is preloaded, so you can use
 \verb+\begin{enumerate}[(a)]+ or the like.)
\item Do not use ``self-made'' sectioning commands (e.\,g., \verb+\noindent{\bf My+ \verb+Paragraph}+).
\item Do not hide large text blocks using comments or \verb+\iffalse+ $\ldots$ \verb+\fi+ constructions.
\item Do not use conditional structures to include/exclude content. Instead, please provide only the content that should be published -- in one file -- and nothing else.
\item Do not wrap figures and tables with text. In particular, the package \texttt{wrapfig} is not supported.
\item Do not change the bibliography style. In particular, do not use author-year citations. (The
\texttt{natbib} package is not supported.)
\end{itemize}

\enlargethispage{\baselineskip}

This is only a summary containing the most relevant details. Please read the complete document ``LIPIcs: Instructions for Authors and the \texttt{lipics-v2019} Class'' for all details and don't hesitate to contact Dagstuhl Publishing (\url{mailto:publishing@dagstuhl.de}) in case of questions or comments:
\href{http://drops.dagstuhl.de/styles/lipics-v2019/lipics-v2019-authors/lipics-v2019-authors-guidelines.pdf}{\texttt{http://drops.dagstuhl.de/styles/lipics-v2019/\newline lipics-v2019-authors/lipics-v2019-authors-guidelines.pdf}}

\section{Lorem ipsum dolor sit amet}

Lorem ipsum dolor sit amet, consectetur adipiscing elit \cite{DBLP:journals/cacm/Knuth74}. Praesent convallis orci arcu, eu mollis dolor. Aliquam eleifend suscipit lacinia. Maecenas quam mi, porta ut lacinia sed, convallis ac dui. Lorem ipsum dolor sit amet, consectetur adipiscing elit. Suspendisse potenti. Donec eget odio et magna ullamcorper vehicula ut vitae libero. Maecenas lectus nulla, auctor nec varius ac, ultricies et turpis. Pellentesque id ante erat. In hac habitasse platea dictumst. Curabitur a scelerisque odio. Pellentesque elit risus, posuere quis elementum at, pellentesque ut diam. Quisque aliquam libero id mi imperdiet quis convallis turpis eleifend.

\begin{lemma}[Lorem ipsum]
\label{lemma:lorem}
Vestibulum sodales dolor et dui cursus iaculis. Nullam ullamcorper purus vel turpis lobortis eu tempus lorem semper. Proin facilisis gravida rutrum. Etiam sed sollicitudin lorem. Proin pellentesque risus at elit hendrerit pharetra. Integer at turpis varius libero rhoncus fermentum vitae vitae metus.
\end{lemma}

\begin{proof}
Cras purus lorem, pulvinar et fermentum sagittis, suscipit quis magna.

\begin{claim}
content...
\end{claim}
\begin{claimproof}
content...
\end{claimproof}

\end{proof}

\begin{corollary}[Curabitur pulvinar, \cite{DBLP:books/mk/GrayR93}]
\label{lemma:curabitur}
Nam liber tempor cum soluta nobis eleifend option congue nihil imperdiet doming id quod mazim placerat facer possim assum. Lorem ipsum dolor sit amet, consectetuer adipiscing elit, sed diam nonummy nibh euismod tincidunt ut laoreet dolore magna aliquam erat volutpat.
\end{corollary}

\begin{proposition}\label{prop1}
This is a proposition
\end{proposition}

\autoref{prop1} and \cref{prop1} \ldots

\subsection{Curabitur dictum felis id sapien}

Curabitur dictum \cref{lemma:curabitur} felis id sapien \autoref{lemma:curabitur} mollis ut venenatis tortor feugiat. Curabitur sed velit diam. Integer aliquam, nunc ac egestas lacinia, nibh est vehicula nibh, ac auctor velit tellus non arcu. Vestibulum lacinia ipsum vitae nisi ultrices eget gravida turpis laoreet. Duis rutrum dapibus ornare. Nulla vehicula vulputate iaculis. Proin a consequat neque. Donec ut rutrum urna. Morbi scelerisque turpis sed elit sagittis eu scelerisque quam condimentum. Pellentesque habitant morbi tristique senectus et netus et malesuada fames ac turpis egestas. Aenean nec faucibus leo. Cras ut nisl odio, non tincidunt lorem. Integer purus ligula, venenatis et convallis lacinia, scelerisque at erat. Fusce risus libero, convallis at fermentum in, dignissim sed sem. Ut dapibus orci vitae nisl viverra nec adipiscing tortor condimentum \cite{DBLP:journals/cacm/Dijkstra68a}. Donec non suscipit lorem. Nam sit amet enim vitae nisl accumsan pretium.

\begin{lstlisting}[caption={Useless code},label=list:8-6,captionpos=t,float,abovecaptionskip=-\medskipamount]
for i:=maxint to 0 do
begin
    j:=square(root(i));
end;
\end{lstlisting}

\subsection{Proin ac fermentum augue}

Proin ac fermentum augue. Nullam bibendum enim sollicitudin tellus egestas lacinia euismod orci mollis. Nulla facilisi. Vivamus volutpat venenatis sapien, vitae feugiat arcu fringilla ac. Mauris sapien tortor, sagittis eget auctor at, vulputate pharetra magna. Sed congue, dui nec vulputate convallis, sem nunc adipiscing dui, vel venenatis mauris sem in dui. Praesent a pretium quam. Mauris non mauris sit amet eros rutrum aliquam id ut sapien. Nulla aliquet fringilla sagittis. Pellentesque eu metus posuere nunc tincidunt dignissim in tempor dolor. Nulla cursus aliquet enim. Cras sapien risus, accumsan eu cursus ut, commodo vel velit. Praesent aliquet consectetur ligula, vitae iaculis ligula interdum vel. Integer faucibus faucibus felis.

\begin{itemize}
\item Ut vitae diam augue.
\item Integer lacus ante, pellentesque sed sollicitudin et, pulvinar adipiscing sem.
\item Maecenas facilisis, leo quis tincidunt egestas, magna ipsum condimentum orci, vitae facilisis nibh turpis et elit.
\end{itemize}

\begin{remark}
content...
\end{remark}

\section{Pellentesque quis tortor}

Nec urna malesuada sollicitudin. Nulla facilisi. Vivamus aliquam tempus ligula eget ornare. Praesent eget magna ut turpis mattis cursus. Aliquam vel condimentum orci. Nunc congue, libero in gravida convallis \cite{DBLP:conf/focs/HopcroftPV75}, orci nibh sodales quam, id egestas felis mi nec nisi. Suspendisse tincidunt, est ac vestibulum posuere, justo odio bibendum urna, rutrum bibendum dolor sem nec tellus.

\begin{lemma} [Quisque blandit tempus nunc]
Sed interdum nisl pretium non. Mauris sodales consequat risus vel consectetur. Aliquam erat volutpat. Nunc sed sapien ligula. Proin faucibus sapien luctus nisl feugiat convallis faucibus elit cursus. Nunc vestibulum nunc ac massa pretium pharetra. Nulla facilisis turpis id augue venenatis blandit. Cum sociis natoque penatibus et magnis dis parturient montes, nascetur ridiculus mus.
\end{lemma}

Fusce eu leo nisi. Cras eget orci neque, eleifend dapibus felis. Duis et leo dui. Nam vulputate, velit et laoreet porttitor, quam arcu facilisis dui, sed malesuada risus massa sit amet neque.

\section{Implications for Verification \label{sec:Implications}}

The coupled phase transitions in the chemical reaction network $\mathbf{N_2}$ make it difficult to verify its behavior.  In this section we describe the use and limitations of verifying the chemical reaction network using simulation, model checking and differential equations.   None of these methods detected that the system turned red when the population reached $2^m$.  We then describe how the use of an interactive theorem prover enabled us to verify the chemical reaction network's behavior at both phase transitions, i.e., that it turned from blue to red at $2^m$ and from red to blue at $2^n$.   The fact that theorem proving could verify behavior that was otherwise not verified for the  chemical reaction network suggests that interactive theorem proving may have a useful role to play in future verification of a class of chemical reaction networks.
Recall that the chemical reaction networks $\mathbf{N_1}$ and $\mathbf{N_2}$ have fixed populations throughout any given execution, and that their initial states have $z_0$ as the entire population.

\subsection {Simulation}

The MATLAB SimBiology package is widely used to explore the behavior of a number of devices (molecules) executing concurrently \cite{matlab2019}. Using SimBiology, simulations of the $\mathbf{N_2}$ chemical reaction network were performed on an Intel processor computer with a processor clock of 5.0 GHz and 64GB of RAM.
Several simulations were performed with increasing  populations $z_0$.
With a population of $10^{7}$, the simulation performed as expected.
However, with a population of $10^{8}$, the simulation failed and terminated with no output or error message.
Thus,
the stochastic simulation was unable to detect that the behavior of the $\mathbf{N_2}$ chemical reaction network could experience a phase transition.

\subsection{Model Checking}

The chemical reaction network $\mathbf{N_2}$  simulated in SimBiology and described above also was verified using the PRISM 4.6 probabilistic model checker \cite{cKwNoPa11}.
Kwiatkowska and Thachuk, among others, have described the use of PRISM for the probabilistic verification of chemical reaction networks for biological systems \cite{jKwiTha14}.

To verify the chemical reaction network behavior we first converted the $\mathbf{N_2}$   model to SBML using the export function in SimBiology, and then converted the SBML model to PRISM using the sbml2prism conversion tool supplied with the PRISM software.  PRISM was used to verify six key properties of the $\mathbf{N_2}$ chemical reaction network at multiple populations. For example, one of the properties stated that  ``$P>=1[\text{F G } r = 0]$'', i.e., that with probability 1, the eventual state of the $R$ species has $0$ molecules, and never changes from that.
With a population of 100, PRISM generated the CTMC state model in 1.65 seconds using the same processor and memory as for the SimBiology simulations, and
the verification of the six properties required less than 2 seconds of CPU time.

For a population of 100 molecules, 97 correctly turn blue and 0 correctly turn red, since the latter only happens when the initial population is larger than $2^{34}$. PRISM also verified that in the final state the species count was $z_0 = 0$, $z_1 = 0$, $z_2 = 1$ and $z_5 = 1$, based on the binary expansion of one hundred.

However, we were unable to model check $\mathbf{N_2}$ with a population of 400
due to the rapid increase in states and limited memory. Thus, model checking confirmed the expected behavior of the $\mathbf{N_2}$ chemical reaction network for a population of $100$ but could not detect the behavioral change to red when the population increased.

Advanced methods to prune a model so that meaningful model checking can occur include symmetry reduction \cite{cHKNPT06},  statistical model checking \cite{jCaKwWh18}, and automated partial exploration of the model \cite{jPaBrUc16}.  Recent work by Cauchi, et al. using formal synthesis allowed verification of systems with 10 continuous variables \cite{cCLLAKC19}.
However, even these methods would not be likely to help with the exceedingly large number of states  when the number of molecules is scaled to a realistic value for experiments.
\color{black}

\subsection{Differential Equations}

We have seen how model checking and simulation fail to detect the ``red'' behavior in our chemical reaction network $\mathbf{N_2}$ due to the processing time and memory required for a large population.  The red behavior also is not detected when $\mathbf{N_2}$
is approximated by deterministic semantics, and in this case it is not due to computational power.  In this model, a chemical reaction network is represented by a system of polynomial autonomous differential equations.   A mathematical connection between the stochastic model and the deterministic model is given by Kurtz \cite{jKurt72}, where he shows that the stochastic model is equivalent to the deterministic model as the number of molecules in the system grows towards infinity.

In general, the system of differential equations induced by a chemical reaction network is difficult or impossible to solve exactly, and numerical methods are often used to approximate solutions. Here, we utilized MATLAB and the SimBiology package \cite{matlab2019} to numerically integrate the system of differential equations for $\mathbf{N_2}$.  The result found that $\mathbf{N_2}$  terminated in a predominantly blue state, again missing the red behavior.

\subsection{Theorem Proving}
\label{sec:TheoremProving}

The simulation, model checking, and differential equations approaches to chemical reaction network verification outlined above all make some simplifying assumptions: reduced state space or generalization to the continuum.
In the case of our chemical reaction network, these assumptions lead to an incorrect verification result.

Interactive theorem proving, however, offers an exact approach that is guaranteed to apply at every scale.
In the interactive theorem proving paradigm, users create a machine-checkable mathematical proof of verification properties in collaboration with a software system.
Model checking also constructs a mathematical proof of correctness, but it relies more on a complete or semi-complete search of the state space in question.
By contrast, the goal of interactive theorem proving is to construct a more traditional mathematical proof that is also machine-checkable.
The result then applies to any population scale; a mathematical proof parameterized by population $N$ is valid at every possible value of $N$.

In a typical interactive theorem proving session, a user starts with a base of trusted facts generated from axioms and assumptions, and uses well-understood rules like modus ponens and double negation removal to construct new trusted facts and lemmas.
As with a conventional mathematical proof, the user's goal is to add new trusted facts in a strategic way until reaching the goal of the proof.

We have verified our chemical reaction network with Isabelle/HOL \cite{oNipKle14,oNiPaWe02}, a popular interactive theorem prover with several useful proof automation features.
Instead of working at the level of rules like modus ponens, users can instruct Isabelle to execute more general proof methods that can apply sequences of basic rules without user direct input.
For example, Isabelle can often prove the equivalence of predicate logic formulas with only one user-generated method invocation.
Once invoked, such a method attempts to automatically construct a series of low-level logical rules whose application proves the equivalence.
An Isabelle proof, then, consists of a directed acyclic graph of facts, connected by applications of these methods.
The user's task is to choose a chain of intermediate goal facts in a way that allows Isabelle to connect them easily on the way to the overall goal.

Isabelle also provides the powerful Sledgehammer automation tool, which makes calls to external proof systems to automate aspects of proof creation.  Sledgehammer takes a goal fact as input and attempts to generate a method invocation that proves it, operating at one level of abstraction above the proof methods invocations discussed above.
Since it is often unclear which method to invoke (or which arguments to supply to it), this functionality can increase proof construction speed substantially.

\begin{figure}
	\begin{center}
		\framebox{\includegraphics[width=3.0in,bb=0 0 645 615]{body/isabelleresults_cropped.png}}
		\caption{\label{fig:isabelleresult}
		The end of the Isabelle proof, which summarizes its results in three lemmas.  The \texttt{context} statements bring our assumptions about the value of $N$ into context.  The \texttt{using} statements bring in trusted facts from the rest of our proof and supply them as arguments to Isabelle's \texttt{auto} proof method.  The identifier \texttt{p} refers to an arbitrary trajectory that is part of each context.  Isabelle displays all statements with a white or light gray background to indicate that it has checked them completely, and they are valid.}
	\end{center}
\end{figure}

We have used Isabelle to verify that our chemical reaction network has the desired behavior for all possible initializations.
That is, if we initialize it with $N<2^{34}$ or $N \ge 2^{67}$, the chemical reaction network terminates with majority blue, but if we initialize it with $2^{34} \le N < 2^{67}$, it terminates with majority red.
As expected, theorem proving is able to verify behavior correctly in all regions, including the middle region that is inaccessible to model checking, simulation, and ODE methods.
Figure~\ref{fig:isabelleresult} shows an image taken from the end of our Isabelle proof; it contains the three goal facts that we successfully verified, which summarize the behavior of the chemical reaction network.

Our Isabelle proof is loosely based on the proofs presented in Sections~\ref{sec:SinglePhaseTransition} and \ref{sec:CoupledPhaseTransitions}.
Whereas those proofs define two chemical reaction networks $\mathbf{N_1}$ and $\mathbf{N_2}$, we use Isabelle's \textit{locale} feature to associate assumptions about the population of $N$ with various parts of our proof.
In the locale where $N < 2^{35} $, for example, we are able to prove that our chemical reaction network terminates with majority blue.
Figure~\ref{fig:isabelleresult} shows how we enter these locales at the end of the proof to bring together our final results.

We refer to the three final locales as the lower blue region, the middle red region, and the upper blue region.
For each region, our proof must show both termination and correctness; i.e., we must show that our chemical reaction network reaches a final state where no reactions are possible, and that any possible final state has the specified red or blue population.
\begin{figure}
	\begin{center}
		\framebox{\includegraphics[height=3.0in]{body/isabelleex.pdf}}
		\caption{\label{fig:isabellecode} This Isabelle code defines a terminal state as a state with no outgoing reactions; $K$ is a relation that encodes which state transitions our reaction set allows.  We also show a sample lemma that helps prove termination: if we identify a countdown expression $f$ and a constant $C$ such that all states with $f < C$ are terminal, then our system is guaranteed to terminate.}
	\end{center}
\end{figure}

As in Lemma~\ref{lem:1QS1}, we show termination in the lower two regions via a ``countdown'' expression that is guaranteed to decrease with every reaction.
See Figure~\ref{fig:isabellecode} for our Isabelle definitions of termination and a general lemma we proved that allows us to use the countdown technique.
In the upper blue region, it is impossible to prove termination without assuming that executions are fair.
Our Isabelle proof includes Equation~\ref{eqn:fairness} as an unproven assumption; we are not interested in unfair trajectories, but since they exist we cannot prove that all trajectories are fair.
For convenience, we also include Observation~\ref{obs:reactionfairness} as an an assumption.
These two fairness assumptions allow us to prove that our chemical reaction network terminates in the upper blue region as well.

Our correctness proofs rely heavily on the sum
$S_{68}=\sum_{i=0}^{67} 2^i z_i$, using the notation of Section~\ref{sec:SinglePhaseTransition}, which is an invariant in the lower two regions.
In the upper blue region, it is an invariant until at least one $Z_{67}$ is produced.
This invariant allows us to reason about the composition of terminal states.
In the lower blue region, for example, we know that no red can ever be produced; the chemical reaction network can only produce its first red molecule alongside $Z$ species that would make the invariant too large.
Following the proof of Theorem~\ref{thm:1QS8}, then, we prove that any terminal state must be majority blue.

\section{Coupled Phase Transitions \label{sec:CoupledPhaseTransitions}}
Let $m, n, p$, and $\mathbf{N_1}$ be as in Section~\ref{sec:singlethreshold}, and let $\mathbf{N_2}$ be a CRN consisting of the $n+2$ reactions of $\mathbf{N_1}$ and the \textit{$\omega$-reaction}
\begin{equation*}
    \omega \equiv R + Z_n \rightarrow B + Z_n.
\end{equation*}
This section proves that $\mathbf{N_2}$ exhibits two coupled population-induced phase transitions as described in the introduction.

We use the same initialization for $\mathbf{N_2}$ as for $\mathbf{N_1}$.  Again, all our results hold regardless of the rate constants of the $n+3$ reactions of $\mathbf{N_2}$.

Routine inspection verifies the following.
\begin{observation}
Lemma~\ref{lem:1QS2} and Corollaries~\ref{cor:1QS3}-\ref{cor:1QS7} hold for $\mathbf{N_2}$ as well as for $\mathbf{N_1}$.
\end{observation}

If $p<2^n$, then Corollary~\ref{cor:1QS4} tells us that $z_n$ never becomes positive in $\mathbf{N_2}$, so the $\omega$-reaction never occurs in $\mathbf{N_2}$.  Thus, for $p<2^n$, $\mathbf{N_2}$ behaves exactly like $\mathbf{N_1}$.

On the other hand, if $p \ge 2^n$, then the behavior of $\mathbf{N_2}$ is very different from that of $\mathbf{N_1}$.  For example, in contrast with Lemma \ref{lem:1QS1}, we have the following.
\begin{lemma}
\label{lem:lemma12}
If $p \ge 2^n$, then not all trajectories of $\mathbf{N_2}$ terminate.
\end{lemma}

\begin{proof}
    Assume that $p \geq 2^n$.
    Let
    \[\vec{\zeta} = \zeta_0^{2^{n-1}}\zeta_1^{2^{n-2}}\dots\zeta_{n-1}^{2^0}\]
    denote a sequence consisting of $2^{n-1}$ consecutive occurrences of the reaction $\zeta_0$, followed by $2^{n-2}$ occurrences of $\zeta_1$, etc.
    Since $p \geq 2^n$ each of these $2^n-1$ reactions is enabled when its turn comes.
    After the sequence $\vec{\zeta}$ has occurred, we have
    \begin{align*}
        z_0 &= p - 2^n,\\
        z_1 &= \dots = z_{n-1} = 0,\\
        z_n &= 1,\\
        b &= \sum_{i = 0}^{m-1} 2^{n-(i+1)} = 2^n (1-2^{-m}),\\
        r &= \sum_{i = m}^{n-1} 2^{n-(i+1)} = 2^{n-m} - 1.
    \end{align*}
    Recalling that $n > m + 1$, we have $r \geq 3$ here, so the reaction $\omega$ is enabled after $\vec{\zeta}$ has occurred.
    In fact $\vec{\zeta}$ can (in principle) be followed by the infinite sequence
    \[\omega, \chi, \omega, \chi, \dots\]
    of reactions, so $\bfNt$ has a nonterminating trajectory.
\end{proof}

It is easy to see that the infinite trajectory of $\bfNt$ exhibited in the proof of Lemma \ref{lem:lemma12} is not fair.
In fact, we prove below that all fair paths of $\bfNt$ terminate.
First, however, we note that $\bfNt$, like $\bfN$, has a unique terminal state.

Let $\varepsilon$ be as defined before Theorem~\ref{thm:1QS8}.
\begin{lemma}
    \label{lem:lemma13}
    If $p \geq 2^n$ and $\bfNt$ terminates, then it does so in the state $(\zs,b,r)$ specified as follows.
    \begin{enumerate}[(i)]
        \item $z_{n-1}\cdots z_0$ is the $n-$bit binary expansion of $p \bfmod 2^n$.
        \item $z_n = 1$.
        \item $b = p - \varepsilon$.
        \item $r = 0$.
    \end{enumerate}
\end{lemma}
\begin{proof}
    Let $q$ be an accessible state of $\bfNt$ that is terminal.
    The proofs of (i) and (ii) are the same as in Theorem~\ref{thm:1QS8}, together with the fact that the $\omega-$reaction does not alter the value of $z_n$.
    Since $z_n = 1$ and the $\omega-$reaction is disabled in state $q$, (iv) holds in $q$.
    Finally, since
    \[p = \sum_{i=0}^n z_i + b + r = \varepsilon + b + r,\]
    (iii) follows from (i), (ii), and (iv).
\end{proof}
\begin{lemma}
    \label{lem:fairimpliesdisable}
    On any fair trajectory of $\bfNt$, after finitely many steps, all $\zeta$-reactions are permanently disabled.
\end{lemma}
\begin{proof}
    For each $0 \leq j \leq n$, let $\Phi_j$ be the assertion that, on any fair trajectory of $\bfNt$, after finitely many steps the reaction $\zeta_j$ is permanently disabled.
    It suffices to prove that $\Phi_j$ holds for all $0 \leq j \leq n$.
    We do this by induction on $j$.

    Let $0 \leq j \leq n$ and assume that $\Phi_i$ holds for all $0 \leq i < j$.
    It suffices to show that $\Phi_j$ holds.
    For this, let $\tau = (q_i | 0 \leq i \leq \infty)$ be a trajectory in which $\zeta_j$ is enabled infinitely often.
    It suffices to show that $\tau$ is not fair.
    We have two cases.
    \begin{case}
        Some $\zeta_i$ for $0 \leq i < j$ is enabled infinitely often.
        Then $\tau$ is not fair by the induction hypothesis.
    \end{case}
    \begin{case}
        There exists $k^* \in \mathbb{N}$ such that, for all $k \geq k^*$ the reactions $\zeta_i$, for $0 \leq i < j$, are all disabled in $q_k$.
        Then $z_j$ does not increase at any step of $\tau$ from $k^*$ onward.
        Since every occurrence of $\zeta_j$ decreases $z_j$, this implies that $\zeta_j$ only occurs finitely many times after $k^*$, hence only finitely many times in $\tau$.
        Since $\zeta_j$ is enabled infinitely often along $\tau$ it follows by Observation 1 that $\tau$ is not fair. \qedhere
    \end{case}
    \end{proof}
\begin{lemma}
    \label{lem:chiomegaterminal}
    With any initialization, all fair trajectories of the chemical reaction network $\textbf{N}{\chi\omega}$, consisting of just the reactions $\chi$ and $\omega$, are terminal.
\end{lemma}
\begin{proof}
    If $\textbf{N}{\chi\omega}$ is initialized with $z_n = 0$, then there is only one full trajectory, which is terminal, so it suffices to prove the lemma for initializations with $z_n > 0$.
    Let $q_0$ be any such initial state, and let $\hat{p}$ be the value of $b+r+z_n$ in $q_0$.
    Since $z_n$ and $\hat{p}$ are invariants of $\textbf{N}{\chi\omega}$, a state of $\textbf{N}{\chi\omega}$ is completely determined by the value of $r$.
    We thus refer to ``the state $r$'' of $\textbf{N}{\chi\omega}$, for $0 \leq r \leq \hat{p}-z_n$.
    Note that in this terminology the unique terminal state is 0.

    For each state $r$ of $\textbf{N}{\chi\omega}$ with initial state $q_0$ the trajectory $\tau_r = (r, r-1, \dots, 1, 0)$ given by $r$ consecutive occurrences of $\omega$ is a terminal trajectory from $r$, so the fair termination lemma (Lemma~\ref{lem:fairterm}) tells us that all fair trajectories of $\textbf{N}{\chi\omega}$ are terminal.
\end{proof}

Recall the notation defined just before Theorem~\ref{thm:1QS8}.  The following result is our main theorem.

\begin{theorem}
    \label{thm:pleq2pownterm}
    Let $(z_0,\dots,z_n,b,r)$ be the state of $\bfNt$ specified as follows.
    \begin{enumerate}[(i)]
        \item $z_{n-1}\cdots z_0$ is the $n$-bit binary expansion of $p \bfmod 2^n$.
        \item $z_n = \llbracket p \geq 2^n \rrbracket$.
        \item $b = (p - \varepsilon) * \llbracket p < 2^m \text{ or } p \geq 2^n \rrbracket$.
        \item $r = (p - \varepsilon) * \llbracket 2^m \leq p < 2^n \rrbracket$.
    \end{enumerate}
    If $p < 2^n$, then $\bfNt$ terminates in this state on all trajectories.
    If $p \geq 2^n$, then $\bfNt$ terminates in this state on all fair trajectories.
\end{theorem}
\begin{proof}
    If $p < 2^n$, then Corollary~\ref{cor:1QS3} tells us that $z_n$ never becomes positive in $\bfNt$, so $\omega$ is never enabled.
    Hence, in this case $\bfNt$ behaves exactly like $\bfN$.
    Theorem~\ref{thm:1QS8} tells us that $\bfNt$ terminates on all trajectories to the state satisfying (i) and (ii) above and, since $\llbracket p < 2^m \rrbracket = \llbracket p < 2^m \text{ or } p \geq 2^n \rrbracket$ and $\llbracket p \geq 2^m \rrbracket = \llbracket 2^m \leq p < 2^n \rrbracket$, also satisfying (iii) and (iv) above.

    If $p \geq 2^n$, then Lemmas~\ref{lem:fairimpliesdisable} and \ref{lem:chiomegaterminal} together tell us that $\bfNt$ terminates on all fair trajectories.
    Since $\llbracket p \geq 2^n \rrbracket = 1,  \llbracket p < 2^m \text{ or } p \geq 2^n \rrbracket =1$, and $\llbracket 2^m \leq p < 2^n \rrbracket = 0$, Lemma~\ref{lem:lemma13} tells us that termination must occur in the state satisfying (i)-(iv) above.
\end{proof}

Since $\varepsilon$ is again negligible with respect to $p$, Theorem~\ref{thm:pleq2pownterm} says that $\bfNt$ terminates in an overwhelmingly blue state if $p < 2^m$ or $p \geq 2^n$ but in an overwhelmingly red state if $2^m \leq p < 2^n$.  Hence $\bfNt$ exhibits very sharp phase transitions at the population thresholds $2^m$ and $2^n$.  As noted in the Introduction and elaborated in Section~\ref{sec:Implications} below, this has significant implications for the verification of chemical reaction networks.
\section{Conclusion}
Taken together, the near-ubiquity of phase transitions in nature \cite{cRanKap10, jCaMiRa18}, the sheer size of molecular populations, and the simplicity of the chemical reaction networks that we have shown to exhibit population-induced phase transitions, indicate that molecular programming will present us with many exceptions to the otherwise useful notion that most bugs can be demonstrated with small counterexamples.  As we have seen, this presents a significant challenge to the verification of chemical reaction networks.  Here we suggest some directions of current and future research that might help meet this challenge.

A great deal of creative work has produced a steady scaling up of model checking to larger and larger state spaces \cite{jClEmSi09, jCDKB18, oAbSiTa18, jBCKL19, cLomPir19, cCJJKVZ19}.  Perhaps the most hopeful approach for dealing with population-induced phase changes, or with more general population-sensitive behaviors, is the model checking of parametrized systems \cite{oAbSiTa18}.

Our results clearly demonstrate the advantage of including theorem proving (by humans and by software) in the verification toolbox for chemical reaction networks and other molecular programming languages.  This in turn suggests that software proof assistants such as Isabelle \cite{oNiPaWe02,oNipKle14} be augmented with features to deal more directly with chemical reaction networks and with population-sensitive phenomena.  It would also be useful to know how much of such work could be carried out with automated theorem provers such as Vampire \cite{cKovVor13}.

Some future programmed molecular applications will be safety-critical, such as in health diagnostics and therapeutics. It is likely that evidence that such systems behave as intended will be required for certification by regulators prior to deployment.  Toward providing such evidence, Nemouchi et al. have recently shown how a descriptive language for safety cases can be incorporated into Isabelle in order to formalize argument-based safety assurance cases \cite{cNFGK19}.

We conclude with a more focused, theoretical question.  Our chemical reaction network $\mathbf{N}_1$ exhibits its phase transition on all trajectories, while $\mathbf{N}_2$ exhibits its coupled phase transitions only on all fair trajectories.  Is there a chemical reaction network that achieves $\mathbf{N}_2$'s coupled phase transitions on {\it all} trajectories?

\section{Chemical Reaction Networks \label{sec:CRN}}

Chemical reaction networks (CRNs) are abstract models of molecular processes in well-mixed solutions.  They are roughly equivalent to three models used in distributed computing, namely, Petri nets, population protocols, and vector addition systems \cite{oCSWB09}.  This paper uses stochastic chemical reaction networks.

For our purposes, a ({\it stochastic}) {\it chemical reaction network} {\bf N} consists of finitely many {\it reactions}, each of which has the form
\begin{equation}
\label{eqn:abcd}
A + B \rightarrow C + D,
\end{equation}
where $A$, $B$, $C$, and $D$ (not necessarily distinct) are {\it species}, i.e., abstract types of molecules.  Intuitively, if this reaction occurs in a solution at some time, then one $A$ and one $B$ disappear from the solution and are replaced by one $C$ and one $D$, these things happening instantaneously.  A {\it state} of the chemical reaction network {\bf N} with species $A_1,\dots,A_n$ at a particular moment of time is the vector $(a_1,\dots,a_s)$, where each $a_i$ is the nonnegative integer count of the molecules of species $A_i$ in solution at that moment.  Note that we are using the so called ``lower-case convention'' for denoting species counts.

In the full stochastic chemical reaction network model, each reaction also has a positive real {\it rate constant}, and the random behavior of {\bf N} obeys a continuous-time Markov chain derived from these rate constants.  However, our results here are so robust that they hold for {\it any} assignment of rate constants, so we need not concern ourselves with rate constants or continuous-time Markov chains.  In fact, for this paper, we can consider the reaction (\ref{eqn:abcd}) to be the if-statement
\begin{equation}
\label{eqn:rxndelta}
\text{if }a>0\text{ and }b>0\text{ then }a, b, c, d := a-1, b-1, c+1, d+1,
\end{equation}
where ``:='' is parallel assignment.   The reaction (\ref{eqn:abcd}) is \textit{enabled} in a state $q$ of $\mathbf{N}$ if $a>0$ and $b>0$ in $q$; otherwise, this reaction is \textit{disabled} in $q$.  A state $q$ of $\mathbf{N}$ is \textit{terminal} if no reaction is enabled in $q$.

A \textit{trajectory} of a chemical reaction network $\mathbf{N}$ is a sequence $\tau = (q_i\ |\ 0 \le i < \ell)$ of states of $\mathbf{N}$, where $\ell \in \mathbb{Z}^+ \cup \{\infty\}$ is the \textit{length} of $\tau$ and, for each $i \in \mathbb{N}$ with $i + 1 < \ell$, there is a reaction of $\mathbf{N}$ that is enabled in $q_i$ and whose effect, as defined by (\ref{eqn:rxndelta}), is to change the state of $\mathbf{N}$ from $q_i$ to $q_{i+1}$.  A trajectory $\tau = (q_i\ |\ 0 \le i < \ell)$ is \textit{terminal} if $\ell < \infty$ and $q_{\ell - 1}$ is a terminal state of $\mathbf{N}$.

Assume for this paragraph that the context specifies an initial state $q_0$ of $\mathbf{N}$, as it does in this paper.  A state $q$ of $\mathbf{N}$ is \textit{accessible} if there is a finite trajectory $\tau = (q_i\ |\ 0 \le i < \ell)$ of $\mathbf{N}$ with $q_{\ell-1} = q$.  A \textit{full trajectory} of $\mathbf{N}$ is a trajectory $\tau = (q_0\ |\ 0 \le i < \ell)$ that is either terminal or infinite.

The fact that each reaction (\ref{eqn:abcd}) has two \textit{reactants} ($A$ and $B$) and two \textit{products} ($C$ and $D$) means that $\mathbf{N}$ is a \textit{population protocol} \cite{jAAER07}.  This condition implies that the total population of all species never changes in the course of a trajectory.  If such a chemical reaction network has $s$ species and initial population $p$, its state space is thus the $(s-1)$-dimensional integer simplex
\begin{equation}
    \Delta^{s-1}(p) = \left\{ (a_1,\dots,a_s) \in \mathbb{N}^s\ \middle|\ \sum_{i=1}^s a_i = p\right\}.
\end{equation}
Note that $|\Delta^{s-1}(p)| = \binom{p+s-1}{s-1}$.  Of course, fewer than this many states may be reachable from a particular initial state of $\mathbf{N}$.

A full trajectory $\tau = (q_i\ |\ 0 \le i < \ell)$ of a CRN $\mathbf{N}$ is (\textit{strongly}) \textit{fair} \cite{jKwia89, oBaiKat08} if it has the property that, for every state $q$ and reaction $\rho$ that is enabled in $q$,
\begin{equation}
\label{eqn:fairness}
    (\exists^\infty i) q_i = q \implies (\exists^\infty j) [q_j = q\ \textrm{and $\rho$ occurs at $j$ in $\tau$}],
\end{equation}
where $(\exists^\infty i)$ means ``there exist infinitely many $i$ such that.''  Note that every terminal trajectory of $\mathbf{N}$ is vacuously fair, because it does not satisfy the hypothesis of (\ref{eqn:fairness}).

The stochastic kinetics of chemical reaction networks implies that, regardless of the rate constants of the reactions, for every population protocol $\mathbf{N}$ and every initial population $p$ of $\mathbf{N}$, there is a real number $\varepsilon>0$ such that, for every state $q$ of $\mathbf{N}$ and reaction $\rho$ that is enabled in $q$, the probability that $\rho$ occurs in $q$ depends only on $q$ and is at least $\varepsilon$.  This in turn implies that, with probability 1, $\mathbf{N}$ follows a fair trajectory.  Hence, if $\mathbf{N}$ has a given behavior on all fair trajectories, then $\mathbf{N}$ has that behavior with probability 1.

We use the following two facts in Section 4.  The first is an obvious consequence of the definition of fairness.
\begin{observation}
\label{obs:reactionfairness}
If $\tau = (q_i\ |\ 0 \le i < \ell)$ is a fair trajectory of a population protocol $\mathbf{N}$, then, for every reaction $\rho$ of $\mathbf{N}$,
\begin{equation}
(\exists^\infty i)[\textrm{$\rho$ is enabled in $q_i$}] \implies (\exists^\infty j)[\textrm{$\rho$ occurs at $j$ in $\tau$}].
\end{equation}
\end{observation}

A famous theorem of Harel \cite{jHare86,oKoze06} implies that the general problem of deciding whether a chemical reaction network terminates on all fair trajectories is undecidable.  Nevertheless, the following lemma gives a useful sufficient condition for termination on all fair trajectories.  This lemma undoubtedly follows from a very old result on fairness, but we do not know a proper reference at the time of this writing.  A proof appears in the Appendix.

\begin{lemma}[fair termination lemma]\label{lem:fairterm} If a population protocol with a specified initial state has a terminal trajectory from every accessible state, then all its fair trajectories are terminal.
\end{lemma}

\section{Single Phase Transition \label{sec:SinglePhaseTransition}}
\label{sec:singlethreshold}
This section presents the chemical reaction network $\mathbf{N}_1$ and proves that it exhibits a population-induced phase transition as described in the introduction.

Fix $m,n,p\in\mathbb{Z}^+$ with $n>m+1$. Let $\mathbf{N}_1$ be a chemical reaction network consisting of the $n+1$ \emph{$\zeta$-reactions}
\[\zeta_i \equiv Z_i+Z_i\to\begin{cases}Z_{i+1}+B&(0\leq i<m)\\Z_{i+1}+R&(m\leq i<n)\\Z_i+R&(i=n)\end{cases}\]
and the \emph{$\chi$-reaction}
\[\chi\equiv B+R\to R+R.\]
All results here hold regardless of the rate constants of these $n+2$ reactions.

We initialize $\mathbf{N}_1$ with $z_0=p$ and all other counts 0.

Intuitively, $B$ is \emph{blue}, $R$ is \emph{red}, and the species $Z_i$ are all \emph{colorless}.

\begin{lemma}\label{lem:1QS1}
	$\mathbf{N}_1$ terminates on all possible trajectories.
\end{lemma}

\begin{proof}
	Every reaction in $\mathbf{N}_1$ reduces the rank
	\[3\sum_{i=0}^n z_i+2b+r.\]
\end{proof}

\begin{notation}
	For $1\leq k\leq n+1$, let
	\[S_k=\sum_{i=0}^{k-1}2^iz_i,\]
	noting that this quantity depends on the state of $\mathbf{N}_1$.
\end{notation}

\begin{lemma}\label{lem:1QS2}
	Let $0\leq j\leq n$ and $1\leq k\leq n+1$.
	\begin{enumerate}
		\item If $j\neq k-1$, then the reaction $\zeta_j$ preserves the value of $S_k$.
		\item If $j=k-1$, then the reaction $\zeta_j$ reduces the value of $S_k$.
	\end{enumerate}
\end{lemma}

\begin{proof}
	Let $0\leq j\leq n$ and $1\leq k\leq n+1$.
	\begin{enumerate}
		\item\label{it:1QS1} This holds trivially if $k\leq j\leq n$, so assume that $0\leq j<k-1$. Let $z_0,\ldots,z_{k-1}$ be the counts of $Z_0,\ldots,Z_{k-1}$ just before an occurrence of $\zeta_j$, let $z'_0,\ldots,z'_{k-1}$ be the counts just after, and let $S'_k=\sum_{i=0}^{k-1}2^i z'_i$. Since $\zeta_j$ occurs, we must have $z_j\geq 2$. If we let $I=\{0,\ldots,k-1\}\setminus\{j,j+1\}$, then each
		\[z'_i=\begin{cases}z_i&\text{if }i\in I\\z_i-2&\text{if }i=j\\z_i+1&\text{if }i=j+1,\end{cases}\]
		so we have
		\[S'_k=\sum_{i\in I}2^i z_i+2^j(z_j-2)+2^{j+1}(z_{j+1}+1)=S_k.\]

		\item Assume that $j=k-1$, and use the notations $z_0,\ldots,z_{k-1}$, $z'_0,\ldots,z'_{k-1}$, and $S'_k$ as in part~\ref{it:1QS1} of this proof. If $1\leq k\leq n$, then each
		\[z'_i=\begin{cases}z_i&\text{if }0\leq i<k-1\\z_i-2&\text{if }i=k-1.\end{cases}\]
		If $k=n+1$ ,then each
		\[z'_i=\begin{cases} z_i&\text{if }0\leq i<k-1\\z_{i-1}&\text{if }i=k-1.\end{cases}\]
		Either way, $S'_k<S_k$.
	\end{enumerate}
\end{proof}

\begin{corollary}\label{cor:1QS3}
	For every $1\leq k\leq n+1$, the inequality $S_k\leq p$ is an invariant of $\mathbf{N}_1$.
\end{corollary}

\begin{proof}
	Let $1\leq k\leq n+1$. We have $S_k=p$ in the initial state that we have specified. The $\chi$-reaction trivially preserves the value of $S_k$ and Lemma~\ref{lem:1QS2} tells us that the reactions $\zeta_0,\ldots,\zeta_n$ all preserve the condition $S_k\leq p$.
\end{proof}

\begin{corollary}\label{cor:1QS4}
	If $1\leq k\leq n$ and $z_k>0$ in some accessible state of $\mathbf{N}_1$, then $p\geq 2^k$.
\end{corollary}

\begin{proof}
	Assume the hypothesis. Then Corollary~\ref{cor:1QS3} tells us that, in the given accessible state,
	\[p\geq S_{k+1}\geq 2^k z_k\geq 2^k.\]
\end{proof}

In the following, for $d\in\mathbb{Z}^+$, we use both the mod-$d$ \emph{congruence} (equivalence relation)
\[a\equiv b\bmod d,\]
which asserts of integers $a,b\in\mathbf{Z}$ that $b-a$ is divisible by $d$, and the \emph{$\mathbf{mod}$-$d$ operation}
\[b\;\mathbf{mod}\;d\]
whose value, for $b\in\mathbb{Z}$, is the unique $r\in\mathbb{Z}$ such that $0\leq r<d$ and $r\equiv b\bmod d$.

\begin{corollary}\label{cor:1QS5}
	The congruence
	\begin{equation}\label{eq:1QSA}
		S_n\equiv p\bmod 2^n
	\end{equation}
	is an invariant of $\mathbf{N}_1$.
\end{corollary}

\begin{proof}
	The initialization of $\mathbf{N}_1$ ensures that (\ref{eq:1QSA}) holds in the initial state. It is clear that the reactions $\zeta_n$ and $\chi$ preserve the value of $S_n$, and Lemma~\ref{lem:1QS2} tells us that the reactions $\zeta_1,\ldots,\zeta_{n-2}$ preserve the value of $S_n$. Hence it suffices to show that the reaction $\zeta_{n-1}$ preserves the truth of (\ref{eq:1QSA}).

	Assume that (\ref{eq:1QSA}) holds just prior to the occurrence of $\zeta_{n-1}$. Let $z_0,\ldots,z_{n-1}$ be the counts of $Z_0,\ldots,Z_{n-1}$ just before this occurrence, let $z'_0,\ldots,z'_{n-1}$ be the counts just after this occurrence, and let $S'_n=\sum_{i=0}^{n-1}2^i z'_i$. Since $\zeta_{n-1}$ occurs, we must have $z_{n-1}\geq 2$. For each $0\leq i<n$ we have
	\[z'_n=\begin{cases}z_i&\text{if }0\leq i<n-1\\z_i-2&\text{if }i=n-1,\end{cases}\]
	so
	\begin{align*}
		S'_n&=\sum_{i=0}^{n-2}2^i z_i +2^{n-1}(z_{n-1}-2)\\
		&=S_n-2^n\\
		&\equiv S_n\bmod 2^n.
	\end{align*}
	Since $S_n\equiv p\bmod 2^n$, it follows that $S'_n\equiv p\bmod 2^n$, i.e., that (\ref{eq:1QSA}) holds just after this occurrence of $\zeta_{n-1}$.
\end{proof}

\begin{corollary}\label{cor:1QS6}
	For every $1\leq k\leq n$, the condition
	\[\Theta_k\equiv z_k=\cdots=z_n=0\implies S_k=p\]
	is an invariant of $\mathbf{N}_1$.
\end{corollary}

\begin{proof}
	Let $1\leq k\leq n$. The condition $\Theta_k$ holds trivially in the initial state that we have specified. The reactions $\zeta_n$ and $\chi$ trivially preserve the value of $S_k$, so let $0\leq j<n$. It suffices to show that $\zeta_j$ preserves the condition $\Theta_k$. For this, assume that $\Theta_k$ holds just prior to an occurrence of $\zeta_j$. Let $z_0,\ldots,z_n$ be the counts of $Z_0,\ldots,Z_n$ just prior to this occurrence of $\zeta_j$, and let $z'_0,\ldots,z'_n$ be the counts just after this occurrence. Since $\zeta_j$ occurs, we must have $z_j\geq 2$ and $z'_{j+1}\geq 1$. To see that $\Theta_k$ holds just after this occurrence of $\zeta_j$, assume that $z'_k=\cdots=z'_n=0$. Then $z_k=\cdots=z_n=0$ and $j+1<k$, so Lemma~\ref{lem:1QS2} tells us that $\zeta_j$ preserves the value of $S_k$. Hence $\Theta_k$ holds just after this occurrence of $\zeta_j$.
\end{proof}

\begin{corollary}\label{cor:1QS7}
	Let $(q_0,\ldots,q_t)$ be a trajectory of $\mathbf{N}_1$, where $q_t$ is a terminal state, and let $1\leq k\leq n$. If $p\geq 2^k$, then there exists $1\leq s\leq t$ such that $z_k>0$ in $q_s$.
\end{corollary}

\begin{proof}
	Let $(q_0,\ldots,q_t)$ be a trajectory of $\mathbf{N}_1$, and let $1\leq k\leq n$. Assume that $p\geq 2^k$ and that there does not exist $s\in\{1,\ldots,t\}$ such that $z_k>0$. It suffices to show that $q_t$ is not terminal.

	Since there does not exist $s\in\{1,\ldots,t\}$ such that $z_k>0$ in $q_s$, it must be the case that $z_k=\cdots=z_n=0$ in $q_t$. It follows by Corollary~\ref{cor:1QS6} that $S_k=p$ holds in $q_t$. Since $\sum_{i=0}^{k-1}z_i=2^{k}-1$ and we have $p\geq 2^k$ by assumption, this implies that there exists $0\leq i<k$ such that $z_i>1$ in $q_t$. Hence the reaction $\zeta_i$ is enabled in $q_t$, so $q_t$ is not terminal.
\end{proof}

\begin{notation}
	For each $r\in\{0,\ldots,2^n-1\}$, let $\lambda(r)$ be the number of 1s in the $n$-bit binary representation of $r$ (leading 0s allowed), and let
	\[\varepsilon=\begin{cases}\lambda(p)&\text{if }p<2^n\\1+\lambda(p\;\mathbf{mod}\;2^n)&\text{if }p\geq 2^n.\end{cases}\]
	Note that $\varepsilon$ is an integer depending on $n$ and $p$, and that $\varepsilon$ is negligible in the sense that $\varepsilon=o(p)$ as $p\to\infty$.
\end{notation}
The boolean value of a condition $\varphi$ is $\llbracket\varphi\rrbracket=\textbf{if }\varphi\textbf{ then }1\textbf{ else }0$.

\begin{theorem}\label{thm:1QS8}
	$\mathbf{N}_1$ terminates on all trajectories in the state $(z_0,\ldots,z_n,b,r)$ specified as follows.
	\begin{enumerate}
		\item\label{it:1QSi} $z_{n-1}\cdots z_0$ is the $n$-bit binary expansion of $p\;\mathbf{mod}\;2^n$.
		\item\label{it:1QSii} $z_n=\llbracket p\geq 2^n\rrbracket$.
		\item\label{it:1QSiii} $b=(p-\varepsilon)\cdot\llbracket p< 2^m\rrbracket$
		\item\label{it:1QSiv} $r=(p-\varepsilon)\cdot\llbracket p\geq 2^m\rrbracket$.
	\end{enumerate}
\end{theorem}

\begin{proof}
	Lemma~\ref{lem:1QS1} tells us that $\mathbf{N}_1$ terminates on all trajectories. Let $q=(z_0,\ldots,z_n,b,r)$ be a terminal state of $\mathbf{N}_1$, and note the following.
	\begin{enumerate}
		\item\label{it:1QSa} For all $0\leq i\leq n$, $\zeta_i$ is not enabled in $q$, so $z_i\in\{0,1\}$.
		\item\label{it:1QSb} $\chi$ is not enabled in $q$, so $b=0$ or $r=0$.
		\item\label{it:1QSc} By (\ref{it:1QSa}), $S_n\leq \sum_{i=0}^{n-1}2^i=2^n-1$, so Corollary~\ref{cor:1QS5} tells us that $S_n=p\;\mathbf{mod}\;2^n$, i.e., that (\ref{it:1QSi}) holds.
		\item\label{it:1QSd} If $p<2^n$, then Corollary~\ref{cor:1QS4} tells us that $z_n=0$. If $p\geq 2^n$, then Corollary~\ref{cor:1QS7} tells us that $z_n\geq 1$ somewhere along every trajectory leading to $q$. Since $z_n$ can never become 0 after becoming positive, this implies that $z_n=1$ in $q$. Hence (\ref{it:1QSii}) holds.
		\item\label{it:1QSe} By (\ref{it:1QSc}) and (\ref{it:1QSd}) we have $\sum_{i=0}^n z_i=\varepsilon$.
		\item\label{it:1QSf} Since $b+r+\sum_{i=0}^n z_i$ is an invariant of $\mathbf{N}_1$, (\ref{it:1QSb}) and (\ref{it:1QSe}) tell us that one of $b$ and $r$ is $p-\varepsilon$ and the other is 0.
		\item \label{it:1QSg} If $p<2^m$, then Corollary~\ref{cor:1QS4} tells us that $z_m=\cdots=z_n=0$ holds throughout every trajectory leading to $q$. This implies that none of the reactions $\zeta_m,\ldots,\zeta_n$ occurs along any trajectory leading to $q$, whence $r=0$.
		\item \label{it:1QSh} If $p\geq 2^m$, then Corollary~\ref{cor:1QS7} tells us that $z_m>0$ holds somewhere along every trajectory leading to $q$. This implies that the reaction $\zeta_{m-1}$ occurs, whence $r$ becomes positive, somewhere along every trajectory leading to $q$. Since $r$ can never become 0 after becoming positive, this implies that $r>0$.
		\item By (\ref{it:1QSf}), (\ref{it:1QSg}), and (\ref{it:1QSh}), (\ref{it:1QSiii}) and (\ref{it:1QSiv}) hold.
	\end{enumerate}
\end{proof}

Since $\varepsilon$ is negligible with respect to $p$, Theorem~\ref{thm:1QS8} says that $\mathbf{N}_1$ terminates in an overwhelmingly blue state if $p < 2^m$ and in an overwhelmingly red state if $p \geq 2^m$.  This is a very sharp phase transition at the population threshold $2^m$.

\section{Introduction}

Chemical reaction networks, mathematical abstractions similar to Petri nets, are used as a programming language to specify the dynamic behaviors of engineered molecular systems.  Existing software can compile chemical reaction networks into DNA strand displacement systems that simulate them with growing generality and precision \cite{cSoSeWi09, jCDSPCS13, cBSJDTW17, jTTBJAC17}.  Programming is a challenging discipline in any case, but this is especially true of molecular programming, because chemical reaction networks---in addition to being Turing universal \cite{jSCWB08,oCSWB09, cFLBP17} and hence subject to all the uncomputable aspects of sequential, imperative programs--are, like the systems that they specify, distributed, asynchronous, and probabilistic.  Since many envisioned applications of molecular programming will be safety critical \cite{oWooLin05,jZhaSee11, jDoBaCh12, jLiLiYa13,jLJLZTS18, jSAGM20, oDiet20}, programmers thus seek to create chemical reaction networks that can be {\it verified} to correctly carry out their design intent.

One principle that is sometimes used in chemical reaction network design is the {\it small population heuristic} \cite{jLPCKP12, cCaKwWh16, jEKLLLM19}.  The idea here is to verify various stages of a design by model checking or software simulation to ferret out bugs in the design prior to laboratory experimentation or deployment.  Since the number of states of a molecular system is typically much larger than its population (the number of molecules present), and since molecular systems typically have very large populations, this model checking or simulation can usually only be carried out on populations that are far smaller than those of the intended molecular systems.  It is nevertheless reasonable to hope that, if a system is going to consist of a very large number of ``devices'' of various sorts, then any unforeseen errors in these devices' interactions will manifest themselves even with very small populations of each device.  It is this reasonable hope that is the underlying premise of the small population heuristic.  (Note that the small population heuristic can be regarded as a molecular version of the small scope hypothesis \cite{jJack19}.)

The question that we address here is whether real molecular systems can thwart the small population heuristic.  That is, can a real molecular system behave very differently at large populations than at small populations?  If so, {\it how sensitive} can its behavior be to its population, and {\it how simple a mechanism} can achieve such sensitivity?

In order to ensure that we are only investigating population effects, we focus our attention on chemical reaction networks that are {\it population protocols} in the sense that their populations remain constant throughout their operations.  If we have such a chemical reaction network, and if we vary its initial population {\it and nothing else}, then we are assured that any resulting variations of behavior are due solely to the differing populations.

In this paper we show that very simple chemical reaction networks can be very sensitive to their own populations.  In fact, they can exhibit {\it population-induced phase transitions}, behaving one way below a threshold population and behaving very differently above that threshold.  After reviewing chemical reaction networks in Section~\ref{sec:CRN}, we present in Section~\ref{sec:SinglePhaseTransition} a chemical reaction network $\mathbf{N}_1$, and we prove that $\mathbf{N}_1$ exhibits a population-induced phase transition in the following sense.  There are two parameters, $m$ and $n$, in the construction.  For this discussion, we may take $m = 34$ and $n = 67$, but the construction is general.  There are $n+1$ reactions among $n+2$ species (molecule types) in $\mathbf{N}_1$.  A species $Z_0$ is given an initial population of $p$, and all other species counts are initially 0.  Each reaction of $\mathbf{N}_1$ has two reactants and two products, so the total population of $\mathbf{N}_1$ is $p$ at all times.  There are in $\mathbf{N}_1$ two distinguished species, $B$ and $R$.  These ``blue'' and ``red'' species are abstract stand-ins for two different behaviors of $\mathbf{N}_1$.  Our construction exploits the inherent nonlinearity of chemical kinetics to ensure that, if $p < 2^m$, then $\mathbf{N}_1$ terminates with essentially all its population blue, while if $p\geq 2^m$, then $\mathbf{N}_1$ terminates with essentially all its population red.  Thus $\mathbf{N}_1$ exhibits a sharp phase transition at the population threshold $p = 2^m$.

Our construction is very simple.  The chemical reaction network $\mathbf{N}_1$ changes its behavior at the threshold $p = 2^m$ by merely computing successive bits of $p$, starting at the least significant bit.  This mechanism is so simple that it could be hidden, by accident or by malice, in a larger chemical reaction network.  Moreover, for suitable values of $m$ (e.g., $m = 34$, so that the threshold $p = 2^m$ is roughly $1.7 \times 10^{10}$),
 \begin{enumerate}
 	\item any attempt to model-check or simulate $\mathbf{N}_1$ will perforce use a population much less than the threshold and conclude that $\mathbf{N}_1$ will always turn blue; while
	\item any realistic wet-lab molecular implementation of $\mathbf{N}_1$ will have a population greater than the threshold and thus turn red.
\end{enumerate}
If the behaviors represented by blue and red here are a desired, ``good'' behavior of $\mathbf{N}_1$ (or of a network containing $\mathbf{N}_1$) and an undesired, ``bad'' behavior of this network, respectively, then the possibility of such a phase transition is a serious challenge to verifying the correct behavior of the chemical reaction network.  Simply put, this is a context in which the small population heuristic can lead us astray.

\begin{figure}[htb]
	\input{body/introfigure}
	\caption{Scales at which different verification methods (simulation, model checking, and ODE's) work.  The gap in the middle shows the scale at which none of these methods will catch the ``produce blue'' behavior of the system design.  This gap is problematic because it is the scale of realistic programmed molecular systems. We show in Section~\ref{sec:TheoremProving} how such systems can be verified using automated theorem proving. \label{fig:introfigure}}
\end{figure}

There is a dual {\it large population heuristic} that is used even more often than the small population heuristic.  A theorem of Kurtz \cite{jKurt72, oAndKur11, oAndKur15} tells us that each {\it stochastic} chemical reaction network (the type of chemical reaction network used in our work here and in most of molecular programming) behaves, at sufficiently large populations, like the corresponding {\it deterministic} chemical reaction network.  Since the behavior of a deterministic chemical reaction network is exactly described by a system of ordinary differential equations, this means that we can use a mathematical software package to numerically solve this system and thereby understand the behavior of the original stochastic chemical reaction network at sufficiently large populations.

In Section~\ref{sec:CoupledPhaseTransitions} we add a single reaction to the chemical reaction network $\mathbf{N}_1$, creating a chemical reaction network $\mathbf{N}_2$ that we prove (in Theorem~\ref{thm:pleq2pownterm}) to exhibit two {\it coupled population-induced phase transitions} in the following sense.  If $p < 2^m$ or $p \geq 2^n$, then $\mathbf{N}_2$ terminates with essentially all its population blue, while if $2^m \leq p < 2^n$, then $\mathbf{N}_2$ terminates with essentially all its population red.  Thus $\mathbf{N}_2$ exhibits sharp phase transitions at the two population thresholds, $p = 2^m$ and $p = 2^n$.  These phase transitions are {\it coupled} in that exceeding the second threshold returns the behavior of $\mathbf{N}_2$ to its behavior below the first threshold.  For suitable values of $m$ and $n$ (e.g. $m = 34$ and $n = 67$ as above, so that the thresholds $p = 2^m$ and $p = 2^n$ are roughly $1.7 \times 10^{10}$ and $1.5 \times 10^{20}$), this implies (see Figure~\ref{fig:introfigure}) that
\begin{enumerate}
	\item any attempt to model-check or simulate $\mathbf{N}_2$ will perforce use a population much less than the smaller threshold and conclude that $\mathbf{N}_2$ will always turn blue, and
 	\item any use of ordinary differential equations to analyze the behavior of $\mathbf{N}_2$ will also conclude that $\mathbf{N}_2$ will always turn blue, a conclusion that is only valid for populations greater than the larger threshold, while
	\item any realistic wet-lab molecular implementation of $\mathbf{N}_2$ will have a population between the two thresholds and thus turn red.
\end{enumerate}
The chemical reaction network $\mathbf{N}_2$ thus exemplifies a class of contexts in which the small population heuristic and the large population heuristic can both lead us astray.

We emphasize that the phase transitions in the chemical reaction networks $\mathbf{N}_1$ and $\mathbf{N}_2$ occur at thresholds in their {\it absolute populations}.  In contrast, phase transitions in chemical reaction networks for approximate majority \cite{jAnAsEi08a, jCarCsi12, cCHKM17} occur at threshold {\it ratios between sub-populations}, and phase transitions in bacterial quorum sensing \cite{jMilBas01} occur at threshold {\it population densities}.

Section~\ref{sec:Implications} discusses the consequences of our results for the verification of programmed molecular systems in some detail.  Here we summarize these consequences briefly.  Phase transitions are ubiquitous in natural and engineered systems \cite{cRanKap10, cRand17, jCaMiRa18}.  Our results are thus cautionary, but they should not be daunting.  Fifteen years after Turing proved the undecidability of the halting problem, Rice \cite{oRice51, jRice53} proved his famous generalization stating that {\it every} nontrivial input/output property of programs is undecidable.  Rice's theorem saves valuable time, but it has never prevented computer scientists from developing specific programs in disciplined ways that enable them to be verified.  Similarly, Sections \ref{sec:SinglePhaseTransition} and \ref{sec:CoupledPhaseTransitions} give mathematical {\it proofs} that the chemical reaction networks $\mathbf{N}_1$ and $\mathbf{N}_2$ have the properties described above, and Section \ref{sec:Implications} describes how we have implemented such proofs in the Isabelle proof assistant \cite{oNiPaWe02, jPaNiWe19}.  As molecular programming develops, simulators, model checkers, theorem provers, and other tools will evolve with it, as will disciplined scientific judgment about how and when to use such tools.

\section{Proof of Fair Termination Lemma}

\begin{lemma}[fair termination lemma]
If a population protocol with a specified initial state has a terminal trajectory from every accessible state, then all its fair trajectories are terminal.
\end{lemma}
\begin{proof}
Let $\mathbf{N}$ be a population protocol with initial state $q_0$, and assume that $\mathbf{N}$ has a terminal trajectory from every accessible state.  Let $\tau = (q_i\ |\ 0 \le i < \infty)$ be an infinite trajectory of $\mathbf{N}$.  It suffices to show that $\tau$ is not fair.

For each state $q$ of $\mathbf{N}$, let
\begin{equation}
    I_q = \{i \in \mathbb{N}\ |\ q_i = q\}.
\end{equation}
Since $\mathbf{N}$ is a population protocol, it has finitely many accessible states, so there is a state $q^*$ of $\mathbf{N}$ such that the set $I_{q^*}$ is infinite.  This state $q^*$ is accessible, so our assumption tells us that there is a finite trajectory $\tau^* = (q_i^*\ |\ 0 \le i < \ell)$ of $\mathbf{N}$ such that $q_0^* = q^*$ and $q^*_{\ell-1}$ is terminal.

Now $I_{q_0^*} = I_{q^*}$ is infinite and $I_{q_{\ell-1}^*} = \emptyset$ (because $q_{\ell-1}^*$ is terminal, so it does not appear in the infinite trajectory $\tau$), so there exists $0 \le k < \ell - 1$ such that $I_{q_k^*}$ is infinite and $I_{q_{k+1}^*}$ is finite.  Let $q^{**} = q_k^*$, and let $\rho$ be the reaction that takes $q_k^*$ to $q_{k+1}^*$.  Then $\rho$ is enabled in $q^{**}$ and there exist infinitely many $i$ such that $q_i = q^{**}$ (because $I_{q^{**}}$ is infinite), but there are only finitely many $j$ for which $q_j = q^*$ and $\rho$ occurs at $j$ in $\tau$ (because $I_{q_{k+1}^*}$ is finite).  Hence $\tau$ is not fair.
\end{proof}

\section*{Acknowledgments} We thank Neil Lutz for technical assistance.  The second and third authors thank Erik Winfree for his hospitality while they did part of this work during a 2020 sabbatical visit at the California Institute of Technology.

\bibliographystyle{plain}

redpajama_set_name: RedPajamaArXiv


Tamarah Ellen of Tamarah's Closet interviewed Karen yesterday on her live YouTube channel. The inverview runs about an hour and 15 minutes. If you'd like to learn a little about Karen's history, her inspirations and her paintings you can view the video here.
It seems as though I'm making a career out of this latest painting, but it's a bike I've wanted to paint for sometime now and I just want to get it right. The underpainting is finally complete and it's on to the next pass. I hope when this piece is finished I'll feel that the time had been well spent.
Last week Karen and I headed to Charleston to deliver 23 paintings to Principle Gallery for her solo show Friday April 7th. It was a really nice drive. As usual we had veganee snacks onboard and and for this trip the Exorcist playing on the iPod.
We arrived around noon, were warmly greeted by Frank, Thomas and Liz, the staff at Principle, and immediately formed a fireman's chain to unload our car. Once the precious cargo was safely in the gallery we all spent some time catching up then Karen and I checked out the current work in the gallery.
We knew that at this moment Atlanta was getting hammered by a terrific storm and it was quickly heading our way, so we dumped our bags and headed out to see the town while the weather was still good. Charleston is such a great walking city, with lots of art galleries. Our first gallery stop is nearly always Robert Lange Studios. Robert and his staff were preparing their gallery for the Friday opening of Brett Scheifflee's solo show. Brett is a great guy and his work was stunning. The images below don't do his work justice. You have to see it in person to truly appreciate its subtle beauty.
After we had walked around for a while it was time to eat, and for us that always means CO on King Street. CO is this wonderful Asian restaurant that offers this addictive Curry Laksa. They have another location in Charlotte, so when we go there for Karen's show in the fall, we'll be having Laksa again.
The remainder of the day was spent wandering. That night the storm hit hard. Fortunately it didn't do any damage and by late morning the sun was back and the forecast for the remainder of the week looked perfect.
After breakfast at Eli's Table (a nice little restaurant right next door to the gallery) the following morning we headed out to the South Carolina Aquarium. Karen's begun to use fish in some of her compositions so it was a must see on this trip. It's a good aquarium and Karen got a couple of hundred photos to work from before we left.
Once we finished up at the aquarium we drove back into town and did the gallery hopping thing, then relaxed on the swing at the Charleston Waterfront Pier. We ended the day with an early dinner at the Brown Dog Deli on Broadstreet. It's a great place to eat with really good vegetarian options and a wonderful hippie vibe to the surroundings.
The next day began with breakfast at Gnome Cafe. Karen and I are always on the lookout for vegan/vegetarian restaurants and this was a real find. Very green, very forward thinking, very tasty and very nice people. In fact halfway through our day we returned for lunch. Side note: I hate Brussel sprouts, but the chef asked me to try a sample of that days Brussell sprouts side item. I held my nose and tried it . . . then ordered it as a side with my sandwich. Delicious.
Fueled for the day we headed out to Sullivan's Island to get in some beach time. We parked next to Fort Moultrie and walked down a sandy path to the shore. The winds that day were practically gale force so walking was a struggle. It wasn't long before our mouths were so full of sand we decided to bale on the beach. On our way back to the path leading to our car we came upon a sea bird laying in the sand near the water. It was alert but didn't move as we approached. We were even able to touch it and realized that it was injured. We weren't sure what to do so I got on the phone and started looking for a "bird rescue" center. About eight calls later I finally found who I was looking for. I described the birds condition and they said they would send someone to come and pick it up. By this time the water was beginning to lap up against the bird so Karen got a beach towel from the car and wrapped it up, and we took it back to our car to wait for the rescue person.
About fifteen minutes later help arrived. The woman said it was a Loon and that they'd seen a number of these birds injured. We thought it may have been hurt during the terrific storm the night before. The woman was very nice, crated the bird and took our contact info to let us know how things turned out. We gave her a donation and she drove away, both of us hoping the bird would be okay. Sadly, we got a call on the phone in the car on the way back to Atlanta from the center and they told us that the bird had died.
Since we were already at Fort Moultrie, and I love me a fort, we did the tour. This was where Edgar Allan Poe was stationed when he was nineteen years old. Cool. The weather was perfect, although like I said very windy. Great for photos though, "severe clear". We walked around and read the plaques. I noticed one strange thing, the flag over the fort was at half staff. I couldn't figure out why so I asked at the visitor center and they said that John Glenn was being buried at Arlington Cemetery that day.
Homage Show at the Vendue Hotel with Karin Jurick's painting, "Moms"
That evening Karen and I went to the opening of the "Homage" show at the Vendue Hotel. We had been to the hotel the day before and met the artist in residence Fred Jamar. An interesting fellow with a good gig. The theme of this show was that artists from various galleries would paint their own versions of classic masterpieces. Our great friend Karin Jurick used Whistlers Mother as her reference and came up with her homage titled "Moms". All of the paintings were very creative, the crowd was large and everyone seemed to be having a good time. A really fun was to spend an evening in Charleston.
Our final day began with a trip to John's Island to see the Angel Oak. Some friends had told us that "you have to go and see this tree", so we did, and it was definitely worth the trip. The tree is claimed to be somewhere between 400 and 500 years old, with an expected lifespan of over 900 years. It's truly spectacular.
While we were there we met an artist painting the tree. His name was Frank De Loach. A very amiable man with an extensive history too broad in scope to list here other than to mention he worked at the Field Museum in Chicago and was involved with the preparation of the Tyrannosaurus Rex "Sue". For an armchair paleontologist like me I thought that was very cool. We talked for a long time and before we left we invited him to Karen's show that night and he said he'd try and make it.
After we left the oak we drove over to Folly Beach. We walked around in the sand for a little while, but like the day before the wind was really strong making it difficult to get around. We eventually wound up on the fishing pier and just admired the view from there.
Our free time was limited that day because Karen's opening was that evening, and we wanted to get in one more bowl of Laksa before we returned to Atlanta, so we drove to our room, got cleaned up and walked back to CO.
A little after 5 we entered the gallery. Frank (the gallery director), Thomas and Liz had done a beautiful job of hanging the show and there was already a sizable crowd as we walked in. One of her collectors got there early and was anxiously waiting to meet Karen. He was a surgeon, attending a conclave in Charleston, and was quickly running out of time before he had to leave. Fortunately we arrived early enough for he and Karen to have time to talk, and also buy a painting before heading out for his meeting.
Eric who usually tends the beverages was there again. It's always good to see him. He served drinks while Frank, Liz and Thomas expertly worked the room.
Frank DeLoach, the artist we had met at the Angel Oak that morning did come to the show.
From then on it was more people, more good wishes, more compliments and more sales. When the opening had ended Karen had sold nine paintings. Frank, with his endless sense of optimism, assured Karen that her show would sell out before it's over.
After the show we went back to our apartment and collapsed. Having a solo show is kind of stressful, so we watched a couple of episodes of House Hunters on the iPad then fell asleep.
We had already said our good-byes at the close of the show the night before and left Charleston early the next morning. It was an easy ride back and our house still intact when we arrived home. Chalk up another really successful trip.
Just a few images of a new motorcycle in progress. Been in the works for a few weeks. Got a way to go just to get the underpainting done. Looking forward to the second pass.


text:
Grejohn Kyei, né le  à Gonesse dans le département du Val-d'Oise, est un footballeur français. Il évolue actuellement au poste d'avant-centre au Clermont Foot 63.

Il est champion de Ligue 2 lors de la saison 2017-2018 et finaliste de la Coupe Gambardella en 2014 avec le Stade de Reims.

Biographie

Stade de Reims
Grejohn Kyei commence à jouer au football dès l'âge de sept ans à Villiers-le-Bel. Il rejoint le centre de formation du Stade de Reims en 2010 à l'âge de quinze ans. Il joue dans toutes les catégories d'âge des équipes de jeunes du club rémois.

À partir de 2012, il fait également partie de la réserve du club, qui évolue d'abord en Division d'honneur puis en CFA 2. Parallèlement, il est finaliste de la Coupe Gambardella en 2014 (défaite 2-0 contre l'AJ Auxerre).

Saison 2014-2015

L'attaquant d'origine ghanéenne signe son premier contrat professionnel avec le club champenois, en , pour une durée de trois ans. Mais sa carrière se trouve retardée un mois plus tard : l'espoir rémois bouscule l'arbitre lors d'une rencontre de la réserve contre Sedan ; sa réaction lui vaut une suspension de sept mois des terrains.

Il joue son premier match professionnel le  contre le Stade rennais en Coupe de France où il inscrit son premier but officiel en équipe première. Le , il participe à son premier match de Ligue 1 contre l'OGC Nice. Ses premières apparitions en Ligue 1, à la fin de la saison 2014-15, sont remarquées, Grejohn Kyei entre trois fois en cours de match et inscrit son premier but de Ligue 1 face au Paris Saint-Germain, le .

Saison 2015-2016

Il démarre la nouvelle saison de la meilleure façon, en jouant les quatre premières journées de Ligue 1. Il effectue deux passes décisives lors du premier match de la saison contre les Girondins de Bordeaux. Il est ensuite titularisé pour la première fois contre le FC Lorient, le , et en profite pour marquer son premier but de la saison. Il marque son deuxième but de la saison contre le Gazélec Football Club Ajaccio. Il inscrit le dernier but rémois de la saison contre l'Olympique lyonnais victoire (4-1).

Saison 2016-2017

Alors que son club est redescendu en Ligue 2, il est courtisé par le Stade rennais, mais le club rémois décide de le conserver.

Il marque son premier but de la saison contre Le Havre en Coupe de la Ligue. Il marque son premier but en championnat contre le Gazélec Ajaccio. Il inscrit son deuxième but de la saison contre l'AJ Auxerre, contre la même équipe au match retour il marque un doublé et permet à son équipe de gagner. Il marque son dernier but de la saison contre le Stade lavallois .

Saison 2017-2018

Lors de la première journée il est titulaire mais ne trouve pas le chemin du filet. Grejohn marque son premier but en championnat contre l'AS Nancy-Lorraine. Très utilisé par son entraîneur durant la saison il est courtisé par de nombreux clubs en Ligue 1 et des clubs néerlandais dont Heerenveen. Il marque son dernier but de la saison contre l'AC Ajaccio permettant à son club d'obtenir la victoire. A la fin de la saison, il fête la montée et le titre du championnat Ligue 2 au stade Auguste-Delaune lors du coup sifflet final de la .

Saison 2018-2019

Le  il joue quelques minutes en remplaçant Pablo Chavarría contre l'OGC Nice en Ligue 1.

Racing club de Lens
Fin , il est prêté au Racing Club de Lens par le Stade de Reims. Il inscrit son premier but et offre la victoire à son équipe le  face à l'AJ Auxerre.

Servette Genève puis Clermont
En 2019, il rejoint le Servette Football Club 1890 où il reste jusqu'au 31 janvier 2022 (son contrat finissait en juin). Il quitte alors Servette pour rejoindre le club de Clermont Foot 63, il rejoint la Ligue 1, il a signé un contrat jusqu'en juin 2022.

Avec l'équipe de France espoirs

Premières sélections en bleuets
Il est appelé en équipe de France espoirs, avec laquelle il marque un but, le  lors de sa première et unique sélection (défaite 3-2 contre l'Islande).

Statistiques

Palmarès
 Finaliste de la Coupe Gambardella en 2014 avec le Stade de Reims
 Champion de France de Ligue 2 en 2018 avec le Stade de Reims

Références

Liens externes

Footballeur français
Footballeur ghanéen
Joueur du Stade de Reims
Joueur du Racing Club de Lens
Joueur du Servette FC
Joueur du Clermont Foot 63
Naissance en août 1995
Naissance à Gonesse

redpajama_set_name: RedPajamaWikipedia


Most of us have had a broken bone at some point in our lives and we can all agree that it is not a pleasant feeling. Our skeletal system, though not fragile, is susceptible to an occasional crack or a full-blown broken bone.
Most fractured bones are just left alone to heal. Wearing a cast and popping painkillers seems to do the trick for most. But in some severe cases, metal plates or screws are needed to repair the bones, making the process painful and drawn out.
With growth in medical technology, 3D printing is seen as the future of manufacturing and is already a common addition to most colleges and laboratories.
Now a newly-developed 3-D printed ceramic implant not only helps mend broken bones, but it turns into natural bone to repair broken parts.
The implant was made by Hala Zreiqat, a professor and researcher at the University of Sydney, Australia, and her colleagues.
The material, which has been under the testing phase for a few years, has shown promising results in healing broken arm bones in rabbits.
Now, the team was successfully able to repair large leg fractures in sheep, displaying the superiority of ceramic 3-D printed implants over conventional fracture treatment.
The eight sheep in the study were able to walk with the implants immediately after surgery, with plaster casts helping stabilize their legs only for the first month.
The researchers saw complete healing in 25 per cent of the fractures after three months; the healing percentage stood at 88 after one year.
X-rays showed that as the real bones grew back, the ceramic implant blended into the bone, said a release by New Scientist.
Since the early 2010's, scientists across the world have been experimenting with the potential uses of 3-D printing technology, especially in medicine.


text:
ART Is My Oxygen™
INTERVIEWS/PRESS RELEASES
Hashimoto Contemporary Presents: Brian A. Whiteley
Brian A. Whiteley:
I KNOW WHAT YOU DID LAST SUMMER: A MID-CAREER RETROSPECTIVE
January 11th, 2020 - February 1st, 2020
Hashimoto Contemporary is pleased to present I Know What You Did Last Summer: A Mid Career Retrospective, by Brooklyn-based artist Brian A. Whiteley. I Know What You Did Last Summer will be the artists first time exhibiting at Hashimoto Contemporary, which will highlight the various bodies of works and series the artist has been working on for the past decade.
Drawing inspiration from various sources, including his past and the current political climate, I Know What You Did Last Summer features infamous works from Brian A. Whiteley, as well as new works in a variety of medium, including painting, sculpture, fabric works and video works. The exhibition will be presented in a wood paneled installation, reminiscent of the suburban basement in Whiteley's parents home, where he spent a majority of his formative years.
On view will be the notorious Trump Legacy Stone which the artist created in 2016. The piece was initially placed in Central Park on Easter morning in 2016. The epitaph reads, "Made America Hate Again," with the year of death left blank, serving as a reminder that the possibility remains for a more positive legacy.
The piece immediately went viral and led to a two month long secret service investigation, culminating in Whiteley being placed on the Secret Service watch list after interrogations. The piece, and its subsequent story has since been covered internationally by Hyperallergic, The New York Times, ARTnews, Time Magazine and more.
Other notable works on view will be The Vladimir Putin Presidential Portrait (White House in Background), which hung in Donald Trump's Washington, D.C. hotel for a month and various clown suits from Whiteley's video and cemetery performances.
Please join us Saturday, January 11th from 6pm - 8pm for the opening reception of I Know What You Did Last Summer: A Mid-Career Retrospective. The artist will be in attendance. The exhibition will be on view through Saturday, February 1st.
Brian A. Whiteley: I Know What You Did Last Summer: A Mid-Career Retrospective
210 Rivington Street
Opening Night Reception: Saturday, January 11th, 6pm - 8pm
On View: Saturday, January 11th, 2020 - Saturday, February 1st, 2020
Facebook Event Page: www.facebook.com/events/812701092511821/
Hashimoto Contemporary: www.hashimotocontemporary.com
Brian A. Whiteley: brianwhiteleyart.com/
ABOUT THE GALLERY:
Hashimoto Contemporary is located in San Francisco, CA and New York, NY. Our roster consists of an eclectic blend of new contemporary artists. With monthly rotating exhibitions, our programming focuses on a range of painting, sculpture and installation-based work. You can also visit us at a variety of international art fairs in Miami, New York, London, San Francisco and Los Angeles.
Brian Andrew Whiteley is a Brooklyn-based artist creating works that incorporate sculpture, video, new media and performance. He is the author of several viral art projects, most notably for his politically charged works such as the Trump Tombstone and The Vladimir Putin Painting. His large-scale projects manifest themselves as interactive installations, incorporating several forms of media.
His work has been shown at experimental venues and larger institutions, including: The Metropolitan Museum of Art; New York, NY; The Baltimore Museum of Art, Baltimore, MD; The David Owsley Museum of Art, Muncie, IN; Pony Sugar Gallery, Berlin, GR; Spring / Break Art Show, New York, NY; The Clemente Soto Velez Cultural Center, New York, NY; The Boston Center for the Arts, Boston, MA; Bakehouse Art Center, Miami, FL.
Recent projects have garnered press from The New York Times, The NY Daily News, Village Voice, Daily Mail UK, Gothamist, Brooklyn Magazine, Art Net, BBC, Time, Esquire, GQ, Fox, ABC, NBC and NY Magazine.
Whiteley received his masters from the School of Visual Arts and his bachelors at Ball State University.
brian a whiteley
Hashimoto Contemporary Presents: Sandra Chevrier "Cages And The Void Of Colors"
IN FORMATION: Group Show at Hashimoto Contemporary
The Subway Series: Exclusive Interview with Artist Subway Doodle
Lesson 101: #ArtOnLink
Hashimoto Contemporary NY Presents: "Rippling Stone" by artist DALeast
Taglialatella Gallery Presents: "The Art of Friends" by Burton Morris

redpajama_set_name: RedPajamaCommonCrawl


text:
HAND1 () — білок, який кодується однойменним геном, розташованим у людей на короткому плечі 5-ї хромосоми. Довжина поліпептидного ланцюга білка становить 215 амінокислот, а молекулярна маса — 23 627.

Кодований геном білок за функціями належить до активаторів, білків розвитку, фосфопротеїнів.
Задіяний у таких біологічних процесах, як транскрипція, регуляція транскрипції.
Білок має сайт для зв'язування з ДНК.
Локалізований у ядрі. Залучений у розвитку і диференціації 3х ембріологічних ліній — кардіоміоцитів в серці, трофобластів в плаценті та розвитку судин жовткового мішка.

Функції
HAND1 належить до родини білків HAND, члени якої експресуються під час розвитку судинної системи, серцевого нервового хреста, ендокарду (лише HAND2) і епікарду (лише HAND2). HAND1 експресується в зародковому міокарді, де відіграє значну але не до кінця з'ясовану роль в морфогенезі серцевого м'язу.

HAND1 білок працює разом з HAND2 і ефективність морфогенезу серцевого м'яза пов'язана з їх рівнем експресії. Було показано, що порушення розвитку спостерігаються під час надекспресії та пригнічення експресії цих двох генів. На моделях з делецією гену в клітинах нервового хреста не було показано значиних змін, однак зміна фосфорегуляції Hand1 призводить до утворення «заячої губи» а також до загибелі в утробі. Нокаут гену у мишей викликав смерть через порушення розвитоку серця, таких як не завершення з'єднання серця (failed cardiac looping), несиметричний розвиток шлуночків та дефективне формування перегородки між камерами серця. Це може вказувати на участь порушень експресії HAND у багатьох пацієнтів, з вродженими серцевими вадами.

Загалом HAND фактори беруть участь у розвитку правого і лівого шлуночків, артерій аортальної арки, епікарду та ендокарду. А HAND1 експресується також в трофобластах і залучений в процесах ранньої диференціації.

Морфогенез серця
На третьому тижні ембріонального розвитку рудиментальне серце (білатеральна серцева трубка) утворює асиметричну структуру з опуклостями, що представляють собою майбутні шлуночки та передсердя. HAND1 починає експресується в клітинах серцевої зони з усіх сторін серцевої трубки у вентральній зоні каудального сегмента серця та аортальної випуклості, а після цього обмежується зовнішньою кривою лівого шлуночка в стадії замкнутої петлі (див. кардіогенез). HAND2 і HAND1 разом створюють окремі та перекриваючі ділянки експресії, що, вважають, відіграє роль у створенні асиметричних сигналів для розвитку серця на етапі серцевої петлі.

В HAND1 мутантів окрім заячої губи можуть розвинутись кілька типів порушень формування серця. На приклад, на нокаутних мишах виникали дефекти в вентральній перегородці між шлуночками, деформація атріовентрикулярних клапанів, гіпоплазія (недорозвинутість) шлуночків та аномалії з вихідними трактами шлуночків. У людей було показано залежність мутації в HAND1 та виникненням синдрому недорозвинутого лівого боку серця (важка вроджена вада серця).

Розвиток судин у жовтковому мішку
HAND1 експресується в ембріональних позазародкових тканинах, та відіграє роль у розвитку судин жовткового мішку. Точно не відома необхідність HAND1 саме для формування судин, але було показано, що HAND1 сприяє розвитку судинної системи в мішку рекрутуючи гладенькі м'язові клітини в сітку ендотеліоцитів, що перетворює примітивну ендотеліальну капілярну сітку в функціональну судинну систему. Це було показано на HAND1 нокаутній миші, в ембріонах яких був дефект судинної системи жовткового міхура через відсутність судинної оболонки, що призвело до накопичення гематопоетичних клітин в амніоні.

Література

Примітки

Див. також
 Хромосома 5
 HAND2

Транскрипційні фактори


We are now 2/3's of our way through the Toastmasters year. Club subs are due for payment, Area Contests are taking place and there are a wide variety of awards being registered for both the traditional and Pathways programmes.
Since the launch of the 2019 conference in May this year at Waipuna in Auckland, your organising team has been hard at work. We are focussed on the details, making this occasion a memorable first conference for District 112 that is affordable to all.


text:
Финтинеле () — село у повіті Марамуреш в Румунії. Адміністративно підпорядковане місту Тиргу-Лепуш.

Село розташоване на відстані 374 км на північний захід від Бухареста, 33 км на південний схід від Бая-Маре, 72 км на північ від Клуж-Напоки.

Населення
За даними перепису населення 2002 року у селі проживали  осіб, з них 311 осіб (99,4%) румунів. Усі жителі села рідною мовою назвали румунську.

Примітки

Села повіту Марамуреш


The G&G GC16 FFR line of airsoft electric gun (AEG) is G&G newest intermediate level of M4 for 2015. The major feature that separates this M4 from the others on the same level is the rail system. The FFR M4 line features 4 brand new rifles, each equipped with a different length rail system to accommodate the users for each different play style. The FFR comes in 4 variations: 7" rail, 9" rail, 12" rail, and 12" rail with silencer.


text:
Suciu de Sus – wieś w Rumunii, w okręgu Marmarosz, w gminie Suciu de Sus. W 2011 roku liczyła 2450 mieszkańców.

Przypisy

Wsie w okręgu Marmarosz


Let us know your feedback so we can evolve and improve. Andrea says: Dylan was the master of the endless song Log in. Thank you! April 22, at 6: Beginning his legal career in the US, Kim left private practice to work for Yahoo!
The other bits sounded shoe-horned in and didn't work for me, sorry. April 3, at 7: Classical Music Downloads F. September 19, at Does anyone know the one he used on his summary of video. Originally Posted by EdwardBast.
Ooh say goodbye. As well as completing the task at hand, De Neef has proved particularly popular with the outside counsel he instructs. Reset Password Successful. She has helped to form new separate accounts with institutional investors in Korea and the Middle East. Always play videos fullscreen. Younger brother I am not who I appear to be. I cannot believe youve found it! It's not exactly a medley because it was one melody. Meet the team How can my law firm get involved?
Down Wit Us Redman. Most of all, she is quick to emphasise how much she has been empowered by the organisation.
February 16, at 2: Hey guys! Street 2 Street Jayo Felony.
Michelle Koh began her career handling business maintenance contracts at Pidemco Land, which would later merge with DBS Land to become CapitaLand, before studying her law degree via distance learning. Forming lines of horse and steel By even yards march forward. Now every day i think of us in the summer or am i just lost in a dream?
Change Email. I need you so bad.


text:
see more from Make Money
Building a Small Business? We Found the 10 Best Cities for Entrepreneurs
by Kaitlyn Blount
Pictured here is the nighttime skyline of Boise. Idaho's capital boasts an unemployment rate of just 2.1%. Joecho-16/Getty Images
For aspiring entrepreneurs with dreams of starting their own business, the mind tends to go to one region in particular.
You know which one I'm talking about — it's the one that goes hand in hand with the idea of startups: Silicon Valley.
Sure, Silicon Valley might have been a good place to start a business — especially one of the tech variety — once upon a time. But now, the reality is that the cost of living there has become so outrageous that talent can't flourish unless it's being backed by (at least) a six-figure income.
Impossible living conditions shouldn't smother the entrepreneurial spirit. So, in the spirit of National Entrepreneur Month, we decided to round up a list of cities that are not only hotbeds for entrepreneurship but are actually affordable.
Using data from the U.S. Census Bureau, the U.S. Bureau of Labor Statistics and the U.S. Bureau of Economic Analysis, we considered the following factors of the 100 most populous metropolitan areas:
Share of entrepreneurs.
Share of female entrepreneurs.
Earnings of self-employed workers.
Number of new small businesses started (latest data from 2014).
Change in new small businesses between 2004 and 2014.
Cost of living.
Unemployment rate (latest data from September 2018).
Dream of starting your own empire? Get great ideas delivered straight to your inbox in The Penny Hoarder Daily!
The 10 Best Cities for Entrepreneurs and Startups
Maybe you already live in one of the cities that made our list. If so, it might be time to seriously consider moving forward with that dream of owning your own bakery. And if your city didn't make the cut, keep these places in mind if you ever decide to relocate for business purposes.
Earnings: $56,905
Change in new small businesses: 51%
Share of entrepreneurs: 2.9%
St. Louis is home to blues music, good barbecue and that famous arch — maybe you've heard of it. It's also appealing for new businesses and entrepreneurs, considering the city has seen a whopping 51% change in new small businesses over a decade.
The city also clocks in with prices about 6% below the national average and came in second on our list of the best cities for tech jobs that are actually affordable!
The Rocky Mountains, a rugged ever-present backdrop, rise up beyond downtown Colorado Springs. SWKrullImaging/Getty Images
Change in new small businesses: 8.7%
Denver might get a lot of love and attention, but if you drive about an hour south to Colorado Springs, budding business owners can find a more attractive option. The unemployment rate there is equal to the national average, but the city boasts a high share of entrepreneurs and high average earnings for self-employed workers.
The Colorado Springs Chamber and EDC acts as a good local resource for small business owners and aspiring entrepreneurs. And fun fact: Some of the first GPS technology was developed in Colorado Springs! Big shoes to fill — no pressure.
Change in new small businesses: 11.8%
The capital of Idaho joins our list with a 12% change in small businesses between 2004 and 2014. Boise also has the lowest unemployment rate of the cities on our list, well below the national average of 3.7%.
The U.S. Small Business Administration has a Boise district office for local entrepreneurship resources, and Boise State University houses the Idaho Small Business Development Center.
FROM THE MAKE MONEY FORUM
Gig Work Taking Property Photos in the US
Passive Income Strategies
I have a question about those cash game apps from Google Play store?
See more in Make Money or ask a money question
Change in new small businesses: 9%
Dreaming of starting your own business and spending your off time lounging on the beach? You're in luck, because Sarasota, Florida, made our list with a 9% change in new small businesses over a decade.
Sarasota County's Office of Business and Economic Development offers step-by-step information for small business owners, whether it's helping them get established, relocate or expand. An insider tip from Alex Mahadevan, our data journalist who grew up in Sarasota: The HuB, a coworking space for creatives and entrepreneurs, is worth checking out.
Austin's skyline, bathed in pastel sunrise hues, spreads along the shoreline of Lady Bird Lake. RoschetzkyIstockPhoto/Getty Images
Are you surprised to find Austin on our list? Probably not, considering the Texas capital seems to pop up on "Best Places to Live" lists pretty regularly.
Austin is one of the fastest-growing cities in the nation, attracts a high number of young grads and saw a 25% increase in small businesses between 2004 and 2014.
Thoroughbreds aren't the only things winning blue ribbons in this Kentucky city. Lexington makes the cut as one of the best cities for entrepreneurs due to a high percentage of new businesses and the second-highest average earnings for self-employed workers on our list.
Aspiring entrepreneurs can check out the Kentucky Small Business Development Center for information and resources. Who knows? You could be the next Colonel Sanders.
The lights of passing cars illuminate a bright, busy intersection in sprawling Miami. unclegene/Getty Images
Two things that are hot in Miami: the weather and the entrepreneurship scene. This South Florida city has seen a rise in small business and has a high density of entrepreneurs, earning the top spot on our list when it comes to the share of entrepreneurs.
Similar to Sarasota's HuB, CIC Miami is a coworking office space that fosters the entrepreneurial spirit and is worth looking into for resources or networking purposes.
One of life's biggest frustrations is that part of Kansas City is in Missouri and not, well, Kansas — but that's just my opinion. My personal feelings aside, Kansas City earns a spot on our top 10 list thanks to an almost 20% change in small businesses over a decade and its low unemployment rate.
And for entrepreneurs with a soft spot for technology, Kansas City is an even more attractive option. The city snagged the number one spot on our list of best affordable tech cities.
If there's one thing to take away from all of this, it's don't sleep on Utah. With an overall population just over 3 million, the Beehive State's cities are regularly found on "best cities" lists — including some of our own.
In addition to being one of the best cities for entrepreneurship, Provo also saw a 4% uptick in income in 2017, thanks to a healthy retail trade.
Unemployment rate: 3%
What did I say about Utah? Last but certainly not least, Salt Lake City makes our list of entrepreneur cities with a 4.1% share of entrepreneurs in the state's most populous metro area, and the highest average of earnings for self-employed individuals.
Salt Lake City also graced some of our other lists, thanks to its 2.6% growth in hourly pay and 3.5% income growth.
Kaitlyn Blount is a former staff writer at The Penny Hoarder. Alex Mahadevan is a former data journalist at The Penny Hoarder.
January 16, 2020 Looking for a Side Hustle? These 11 Gigs Pay More Than $20 an Hour
by Kristen Pope
January 17, 2020 Use Your Vocal Skills to Record Audiobooks and Make Money as a Voice Actor
by Dana Sitar
January 16, 2020 Thousands of Remote and On-Site Seasonal Jobs Are Open For Tax Season
January 14, 2020 Working for Tips? These Strategies Will Help You Earn Even More
by Steve Gillman
15 Hours Ago Driving for Lyft or Uber? Here's Why You May Want to Consider a Dash Cam